Build Log: bitwuzla-cxx.0.2.0

Processing: [default: loading data] [bitwuzla-cxx.0.2.0: http] [bitwuzla-cxx.0.2.0: extract] -> retrieved bitwuzla-cxx.0.2.0 (https://github.com/bitwuzla/ocaml-bitwuzla/releases/download/0.2.0/bitwuzla-cxx-0.2.0.tbz) [bitwuzla-cxx: dune build] + /home/opam/.opam/default/bin/dune "build" "-p" "bitwuzla-cxx" "-j" "255" "@install" (CWD=/home/opam/.opam/default/.opam-switch/build/bitwuzla-cxx.0.2.0) - (cd _build/default/vendor && /usr/bin/patch -p1 --directory bitwuzla) < _build/default/vendor/patch/0001-api-Add-hook-for-ocaml-z-value.patch - File include/bitwuzla/cpp/bitwuzla.h is read-only; trying to patch anyway - patching file include/bitwuzla/cpp/bitwuzla.h - Hunk #1 succeeded at 793 (offset 77 lines). - File src/lib/bv/bitvector.h is read-only; trying to patch anyway - patching file src/lib/bv/bitvector.h - (cd _build/default/vendor && /usr/bin/patch -p1 --directory bitwuzla) < _build/default/vendor/patch/0002-ocaml-make-NodeManager-global-from-thread-local.patch - File src/node/node_manager.cpp is read-only; trying to patch anyway - patching file src/node/node_manager.cpp - (cd _build/default/vendor && /usr/bin/patch -p1 --directory bitwuzla) < _build/default/vendor/patch/0003-Fix-compilation-with-older-GCC-version.patch - File src/solver/bv/bv_prop_solver.cpp is read-only; trying to patch anyway - patching file src/solver/bv/bv_prop_solver.cpp - (cd _build/default/vendor/cadical && /usr/bin/gcc -x c++ -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -Wall -fdiagnostics-color=always -I/opt/homebrew/include -std=c++11 -DNDEBUG -DNBUILD -g -I /home/opam/.opam/default/lib/ocaml -I src -o decompose.o -c src/decompose.cpp) - src/decompose.cpp: In member function 'bool CaDiCaL::Internal::decompose_round()': - src/decompose.cpp:282:22: warning: array subscript 2 is above array bounds of 'int [2]' [-Warray-bounds=] - 282 | c->literals[l] = clause[l]; - | ~~~~~~~~~~~~~^ - In file included from src/internal.hpp:54, - from src/decompose.cpp:1: - src/clause.hpp:89:9: note: while referencing 'CaDiCaL::Clause::<unnamed union>::literals' - 89 | int literals[2]; // Of variadic 'size' (shrunken if strengthened). - | ^~~~~~~~ - (cd _build/default/api && /usr/bin/gcc -x c++ -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -Wall -fdiagnostics-color=always -std=c++17 -I/opt/homebrew/include -g -I /home/opam/.opam/default/lib/ocaml -I ../vendor/bitwuzla/include -o build_enum_kind.o -c build_enum_kind.cpp) - build_enum_kind.cpp: In function 'void build_enum_kind()': - build_enum_kind.cpp:31:23: warning: comparison of integer expressions of different signedness: 'int' and 'std::__cxx11::basic_string<char>::size_type' {aka 'long unsigned int'} [-Wsign-compare] - 31 | for (int j = 1; j < name.length(); j += 1) - | ~~^~~~~~~~~~~~~~~ - (cd _build/default/api && /usr/bin/gcc -x c++ -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -Wall -fdiagnostics-color=always -std=c++17 -I/opt/homebrew/include -g -I /home/opam/.opam/default/lib/ocaml -I ../vendor/bitwuzla/include -o build_enum_rounding_mode.o -c build_enum_rounding_mode.cpp) - build_enum_rounding_mode.cpp: In function 'void build_enum_rounding_mode()': - build_enum_rounding_mode.cpp:34:23: warning: comparison of integer expressions of different signedness: 'int' and 'std::__cxx11::basic_string<char>::size_type' {aka 'long unsigned int'} [-Wsign-compare] - 34 | for (int j = 1; j < name.length(); j += 1) - | ~~^~~~~~~~~~~~~~~ - (cd _build/default/vendor/cadical && /usr/bin/gcc -x c++ -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -Wall -fdiagnostics-color=always -I/opt/homebrew/include -std=c++11 -DNDEBUG -DNBUILD -g -I /home/opam/.opam/default/lib/ocaml -I src -o lookahead.o -c src/lookahead.cpp) - In file included from src/lookahead.cpp:1: - In constructor 'CaDiCaL::CubesWithStatus::CubesWithStatus(CaDiCaL::CubesWithStatus&&)', - inlined from 'CaDiCaL::CubesWithStatus CaDiCaL::Internal::generate_cubes(int, int)' at src/lookahead.cpp:394:12: - src/internal.hpp:105:8: warning: 'cubes.CaDiCaL::CubesWithStatus::status' may be used uninitialized [-Wmaybe-uninitialized] - 105 | struct CubesWithStatus { - | ^~~~~~~~~~~~~~~ - src/lookahead.cpp: In member function 'CaDiCaL::CubesWithStatus CaDiCaL::Internal::generate_cubes(int, int)': - src/lookahead.cpp:392:21: note: 'cubes' declared here - 392 | CubesWithStatus cubes; - | ^~~~~ - (cd _build/default/vendor/cadical && /usr/bin/gcc -x c++ -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -Wall -fdiagnostics-color=always -I/opt/homebrew/include -std=c++11 -DNDEBUG -DNBUILD -g -I /home/opam/.opam/default/lib/ocaml -I src -o solver.o -c src/solver.cpp) - src/solver.cpp: In destructor 'CaDiCaL::Solver::~Solver()': - src/solver.cpp:261:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare] - 261 | if ((this == 0)) break; \ - | ^~ - src/solver.cpp:350:3: note: in expansion of macro 'TRACE' - 350 | TRACE ("reset"); - | ^~~~~ - src/solver.cpp: In member function 'int CaDiCaL::Solver::vars()': - src/solver.cpp:261:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare] - 261 | if ((this == 0)) break; \ - | ^~ - src/solver.cpp:398:3: note: in expansion of macro 'TRACE' - 398 | TRACE ("vars"); - | ^~~~~ - src/solver.cpp: In member function 'void CaDiCaL::Solver::reserve(int)': - src/solver.cpp:261:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare] - 261 | if ((this == 0)) break; \ - | ^~ - src/solver.cpp:406:3: note: in expansion of macro 'TRACE' - 406 | TRACE ("reserve", min_max_var); - | ^~~~~ - src/solver.cpp: In member function 'bool CaDiCaL::Solver::set(const char*, int)': - src/solver.cpp:261:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare] - 261 | if ((this == 0)) break; \ - | ^~ - src/solver.cpp:453:3: note: in expansion of macro 'TRACE' - 453 | TRACE ("set", arg, val); - | ^~~~~ - src/solver.cpp: In member function 'bool CaDiCaL::Solver::limit(const char*, int)': - src/solver.cpp:261:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare] - 261 | if ((this == 0)) break; \ - | ^~ - src/solver.cpp:493:3: note: in expansion of macro 'TRACE' - 493 | TRACE ("limit", arg, val); - | ^~~~~ - src/solver.cpp: In member function 'void CaDiCaL::Solver::add(int)': - src/solver.cpp:261:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare] - 261 | if ((this == 0)) break; \ - | ^~ - src/solver.cpp:528:3: note: in expansion of macro 'TRACE' - 528 | TRACE ("add", lit); - | ^~~~~ - src/solver.cpp: In member function 'void CaDiCaL::Solver::constrain(int)': - src/solver.cpp:261:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare] - 261 | if ((this == 0)) break; \ - | ^~ - src/solver.cpp:540:3: note: in expansion of macro 'TRACE' - 540 | TRACE ("constrain", lit); - | ^~~~~ - src/solver.cpp: In member function 'void CaDiCaL::Solver::assume(int)': - src/solver.cpp:261:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare] - 261 | if ((this == 0)) break; \ - | ^~ - src/solver.cpp:552:3: note: in expansion of macro 'TRACE' - 552 | TRACE ("assume", lit); - | ^~~~~ - src/solver.cpp: In member function 'int CaDiCaL::Solver::lookahead()': - src/solver.cpp:261:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare] - 261 | if ((this == 0)) break; \ - | ^~ - src/solver.cpp:564:3: note: in expansion of macro 'TRACE' - 564 | TRACE ("lookahead"); - | ^~~~~ - src/solver.cpp:261:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare] - 261 | if ((this == 0)) break; \ - | ^~ - src/solver.cpp:561:3: note: in expansion of macro 'TRACE' - 561 | TRACE ("lookahead"); - | ^~~~~ - src/solver.cpp: In member function 'void CaDiCaL::Solver::reset_assumptions()': - src/solver.cpp:261:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare] - 261 | if ((this == 0)) break; \ - | ^~ - src/solver.cpp:581:3: note: in expansion of macro 'TRACE' - 581 | TRACE ("reset_assumptions"); - | ^~~~~ - src/solver.cpp: In member function 'void CaDiCaL::Solver::reset_constraint()': - src/solver.cpp:261:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare] - 261 | if ((this == 0)) break; \ - | ^~ - src/solver.cpp:589:3: note: in expansion of macro 'TRACE' - 589 | TRACE ("reset_constraint"); - | ^~~~~ - src/solver.cpp: In member function 'int CaDiCaL::Solver::solve()': - src/solver.cpp:261:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare] - 261 | if ((this == 0)) break; \ - | ^~ - src/solver.cpp:630:3: note: in expansion of macro 'TRACE' - 630 | TRACE ("solve"); - | ^~~~~ - src/solver.cpp: In member function 'int CaDiCaL::Solver::simplify(int)': - src/solver.cpp:261:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare] - 261 | if ((this == 0)) break; \ - | ^~ - src/solver.cpp:638:3: note: in expansion of macro 'TRACE' - 638 | TRACE ("simplify", rounds); - | ^~~~~ - src/solver.cpp: In member function 'bool CaDiCaL::Solver::failed(int)': - src/solver.cpp:261:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare] - 261 | if ((this == 0)) break; \ - | ^~ - src/solver.cpp:663:3: note: in expansion of macro 'TRACE' - 663 | TRACE ("failed", lit); - | ^~~~~ - src/solver.cpp: In member function 'bool CaDiCaL::Solver::constraint_failed()': - src/solver.cpp:261:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare] - 261 | if ((this == 0)) break; \ - | ^~ - src/solver.cpp:674:3: note: in expansion of macro 'TRACE' - 674 | TRACE ("constraint_failed"); - | ^~~~~ - src/solver.cpp: In member function 'void CaDiCaL::Solver::phase(int)': - src/solver.cpp:261:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare] - 261 | if ((this == 0)) break; \ - | ^~ - src/solver.cpp:693:3: note: in expansion of macro 'TRACE' - 693 | TRACE ("phase", lit); - | ^~~~~ - src/solver.cpp: In member function 'void CaDiCaL::Solver::unphase(int)': - src/solver.cpp:261:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare] - 261 | if ((this == 0)) break; \ - | ^~ - src/solver.cpp:701:3: note: in expansion of macro 'TRACE' - 701 | TRACE ("unphase", lit); - | ^~~~~ - src/solver.cpp: In member function 'int CaDiCaL::Solver::active() const': - src/solver.cpp:261:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare] - 261 | if ((this == 0)) break; \ - | ^~ - src/solver.cpp:776:3: note: in expansion of macro 'TRACE' - 776 | TRACE ("active"); - | ^~~~~ - src/solver.cpp: In member function 'int64_t CaDiCaL::Solver::redundant() const': - src/solver.cpp:261:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare] - 261 | if ((this == 0)) break; \ - | ^~ - src/solver.cpp:784:3: note: in expansion of macro 'TRACE' - 784 | TRACE ("redundant"); - | ^~~~~ - src/solver.cpp: In member function 'int64_t CaDiCaL::Solver::irredundant() const': - src/solver.cpp:261:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare] - 261 | if ((this == 0)) break; \ - | ^~ - src/solver.cpp:792:3: note: in expansion of macro 'TRACE' - 792 | TRACE ("irredundant"); - | ^~~~~ - src/solver.cpp: In member function 'void CaDiCaL::Solver::freeze(int)': - src/solver.cpp:261:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare] - 261 | if ((this == 0)) break; \ - | ^~ - src/solver.cpp:802:3: note: in expansion of macro 'TRACE' - 802 | TRACE ("freeze", lit); - | ^~~~~ - src/solver.cpp: In member function 'void CaDiCaL::Solver::statistics()': - src/solver.cpp:261:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare] - 261 | if ((this == 0)) break; \ - | ^~ - src/solver.cpp:947:3: note: in expansion of macro 'TRACE' - 947 | TRACE ("stats"); - | ^~~~~ - src/solver.cpp: In member function 'void CaDiCaL::Solver::resources()': - src/solver.cpp:261:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare] - 261 | if ((this == 0)) break; \ - | ^~ - src/solver.cpp:955:3: note: in expansion of macro 'TRACE' - 955 | TRACE ("resources"); - | ^~~~~ - src/solver.cpp: In member function 'void CaDiCaL::Solver::dump_cnf()': - src/solver.cpp:261:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare] - 261 | if ((this == 0)) break; \ - | ^~ - src/solver.cpp:1059:3: note: in expansion of macro 'TRACE' - 1059 | TRACE ("dump"); - | ^~~~~ - src/solver.cpp: In constructor 'CaDiCaL::Solver::Solver()': - src/solver.cpp:261:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare] - 261 | if ((this == 0)) break; \ - | ^~ - src/solver.cpp:339:3: note: in expansion of macro 'TRACE' - 339 | TRACE ("init"); - | ^~~~~ - src/solver.cpp: In member function 'void CaDiCaL::Solver::melt(int)': - src/solver.cpp:261:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare] - 261 | if ((this == 0)) break; \ - | ^~ - src/solver.cpp:810:3: note: in expansion of macro 'TRACE' - 810 | TRACE ("melt", lit); - | ^~~~~ - src/solver.cpp: In member function 'bool CaDiCaL::Solver::frozen(int) const': - src/solver.cpp:261:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare] - 261 | if ((this == 0)) break; \ - | ^~ - src/solver.cpp:820:3: note: in expansion of macro 'TRACE' - 820 | TRACE ("frozen", lit); - | ^~~~~ - src/solver.cpp: In member function 'int CaDiCaL::Solver::fixed(int) const': - src/solver.cpp:261:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare] - 261 | if ((this == 0)) break; \ - | ^~ - src/solver.cpp:684:3: note: in expansion of macro 'TRACE' - 684 | TRACE ("fixed", lit); - | ^~~~~ - src/solver.cpp: In member function 'int CaDiCaL::Solver::val(int)': - src/solver.cpp:261:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare] - 261 | if ((this == 0)) break; \ - | ^~ - src/solver.cpp:651:3: note: in expansion of macro 'TRACE' - 651 | TRACE ("val", lit); - | ^~~~~ - src/solver.cpp: In member function 'CaDiCaL::Solver::CubesWithStatus CaDiCaL::Solver::generate_cubes(int, int)': - src/solver.cpp:261:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare] - 261 | if ((this == 0)) break; \ - | ^~ - src/solver.cpp:572:3: note: in expansion of macro 'TRACE' - 572 | TRACE ("lookahead_cubes"); - | ^~~~~ - src/solver.cpp:261:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare] - 261 | if ((this == 0)) break; \ - | ^~ - src/solver.cpp:569:3: note: in expansion of macro 'TRACE' - 569 | TRACE ("lookahead_cubes"); - | ^~~~~ - (cd _build/default/vendor/bitwuzla && /usr/bin/gcc -x c++ -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -Wall -fdiagnostics-color=always -I/opt/homebrew/include -std=c++17 -Isrc/lib/ -I../cadical/src -I.. -DNDEBUG -g -I /home/opam/.opam/default/lib/ocaml -I include -I src -I src/lib -I ../symfpu -I ../cadical -o solver_engine.o -c src/solver/solver_engine.cpp) - src/solver/solver_engine.cpp: In member function 'void bzla::SolverEngine::ensure_model(const std::vector<bzla::Node>&)': - src/solver/solver_engine.cpp:172:10: warning: unused variable 'res' [-Wunused-variable] - 172 | auto res = solve(); - | ^~~ - (cd _build/default/vendor/bitwuzla && /usr/bin/gcc -x c++ -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -Wall -fdiagnostics-color=always -I/opt/homebrew/include -std=c++17 -Isrc/lib/ -I../cadical/src -I.. -DNDEBUG -g -I /home/opam/.opam/default/lib/ocaml -I include -I src -I src/lib -I ../symfpu -I ../cadical -o normalize.o -c src/preprocess/pass/normalize.cpp) - src/preprocess/pass/normalize.cpp: In member function 'virtual bzla::Node bzla::preprocess::pass::PassNormalize::process(const bzla::Node&)': - src/preprocess/pass/normalize.cpp:1137:16: warning: unused variable 'nm' [-Wunused-variable] - 1137 | NodeManager& nm = NodeManager::get(); - | ^~ -> compiled bitwuzla-cxx.0.2.0 -> installed bitwuzla-cxx.0.2.0 [WARNING] Opam package conf-gmp.5 depends on the following system package that can no longer be found: libgmp-dev