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 - File "api/dune", line 15, characters 9-26: - 15 | (names build_enum_option) - ^^^^^^^^^^^^^^^^^ - (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_option.o -c build_enum_option.cpp) - build_enum_option.cpp: In function 'std::string lng_to_vn(std::string)': - build_enum_option.cpp:24:8: error: 'replace' is not a member of 'std' - 24 | std::replace(vn.begin(), vn.end(), '-', '_'); - | ^~~~~~~ - build_enum_option.cpp: In function 'void build_enum_option()': - build_enum_option.cpp:105:14: error: 'sort' is not a member of 'std'; did you mean 'qsort'? - 105 | std::sort(modes.begin(), modes.end()); - | ^~~~ - | qsort - (cd _build/default/vendor/bitwuzla/src/lib && /usr/bin/gcc -x c++ -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -Wall -fdiagnostics-color=always -I/opt/homebrew/include -std=c++17 -I. -DNDEBUG -g -I /home/opam/.opam/default/lib/ocaml -I bitblast -I bv -I ls -I rng -I util -o aig_bitblaster.o -c bitblast/aig_bitblaster.cpp) - In file included from ./bitblast/aig_bitblaster.h:14, - from bitblast/aig_bitblaster.cpp:11: - ./bitblast/aig/aig_manager.h:109:24: warning: template-id not allowed for constructor in C++20 [-Wtemplate-id-cdtor] - 109 | BitInterface<AigNode>(); - | ^ - ./bitblast/aig/aig_manager.h:109:24: note: remove the '< >' - ./bitblast/aig/aig_manager.h:110:3: warning: template-id not allowed for destructor in C++20 [-Wtemplate-id-cdtor] - 110 | ~BitInterface<AigNode>(); - | ^ - ./bitblast/aig/aig_manager.h:110:3: note: remove the '< >' - (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/bitwuzla/src/lib && /usr/bin/gcc -x c++ -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -Wall -fdiagnostics-color=always -I/opt/homebrew/include -std=c++17 -I. -DNDEBUG -g -I /home/opam/.opam/default/lib/ocaml -I bitblast -I bv -I ls -I rng -I util -o aig_printer.o -c bitblast/aig/aig_printer.cpp) - In file included from ./bitblast/aig/aig_printer.h:14, - from bitblast/aig/aig_printer.cpp:11: - ./bitblast/aig/aig_manager.h:109:24: warning: template-id not allowed for constructor in C++20 [-Wtemplate-id-cdtor] - 109 | BitInterface<AigNode>(); - | ^ - ./bitblast/aig/aig_manager.h:109:24: note: remove the '< >' - ./bitblast/aig/aig_manager.h:110:3: warning: template-id not allowed for destructor in C++20 [-Wtemplate-id-cdtor] - 110 | ~BitInterface<AigNode>(); - | ^ - ./bitblast/aig/aig_manager.h:110:3: note: remove the '< >' - (cd _build/default/vendor/bitwuzla/src/lib && /usr/bin/gcc -x c++ -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -Wall -fdiagnostics-color=always -I/opt/homebrew/include -std=c++17 -I. -DNDEBUG -g -I /home/opam/.opam/default/lib/ocaml -I bitblast -I bv -I ls -I rng -I util -o aig_manager.o -c bitblast/aig/aig_manager.cpp) - In file included from bitblast/aig/aig_manager.cpp:11: - ./bitblast/aig/aig_manager.h:109:24: warning: template-id not allowed for constructor in C++20 [-Wtemplate-id-cdtor] - 109 | BitInterface<AigNode>(); - | ^ - ./bitblast/aig/aig_manager.h:109:24: note: remove the '< >' - ./bitblast/aig/aig_manager.h:110:3: warning: template-id not allowed for destructor in C++20 [-Wtemplate-id-cdtor] - 110 | ~BitInterface<AigNode>(); - | ^ - ./bitblast/aig/aig_manager.h:110:3: note: remove the '< >' - (cd _build/default/vendor/bitwuzla/src/lib && /usr/bin/gcc -x c++ -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -Wall -fdiagnostics-color=always -I/opt/homebrew/include -std=c++17 -I. -DNDEBUG -g -I /home/opam/.opam/default/lib/ocaml -I bitblast -I bv -I ls -I rng -I util -o aig_cnf.o -c bitblast/aig/aig_cnf.cpp) - In file included from ./bitblast/aig/aig_cnf.h:13, - from bitblast/aig/aig_cnf.cpp:11: - ./bitblast/aig/aig_manager.h:109:24: warning: template-id not allowed for constructor in C++20 [-Wtemplate-id-cdtor] - 109 | BitInterface<AigNode>(); - | ^ - ./bitblast/aig/aig_manager.h:109:24: note: remove the '< >' - ./bitblast/aig/aig_manager.h:110:3: warning: template-id not allowed for destructor in C++20 [-Wtemplate-id-cdtor] - 110 | ~BitInterface<AigNode>(); - | ^ - ./bitblast/aig/aig_manager.h:110:3: note: remove the '< >' - (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/src/api/cpp && /usr/bin/gcc -x c++ -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -Wall -fdiagnostics-color=always -I/opt/homebrew/include -std=c++17 -I../.. -I../../lib -I../../../include -DNDEBUG -g -I /home/opam/.opam/default/lib/ocaml -o bitwuzla.o -c bitwuzla.cpp) - In file included from ../../lib/bitblast/aig/aig_cnf.h:13, - from ../../solver/bv/bv_bitblast_solver.h:18, - from ../../solver/bv/bv_solver.h:15, - from ../../solver/solver_engine.h:21, - from ../../solving_context.h:23, - from bitwuzla.cpp:28: - ../../lib/bitblast/aig/aig_manager.h:109:24: warning: template-id not allowed for constructor in C++20 [-Wtemplate-id-cdtor] - 109 | BitInterface<AigNode>(); - | ^ - ../../lib/bitblast/aig/aig_manager.h:109:24: note: remove the '< >' - ../../lib/bitblast/aig/aig_manager.h:110:3: warning: template-id not allowed for destructor in C++20 [-Wtemplate-id-cdtor] - 110 | ~BitInterface<AigNode>(); - | ^ - ../../lib/bitblast/aig/aig_manager.h:110:3: note: remove the '< >' - (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_state.o -c src/solver/solver_state.cpp) - In file included from src/lib/bitblast/aig/aig_cnf.h:13, - from src/solver/bv/bv_bitblast_solver.h:18, - from src/solver/bv/bv_solver.h:15, - from src/solver/solver_engine.h:21, - from src/solver/solver_state.cpp:13: - src/lib/bitblast/aig/aig_manager.h:109:24: warning: template-id not allowed for constructor in C++20 [-Wtemplate-id-cdtor] - 109 | BitInterface<AigNode>(); - | ^ - src/lib/bitblast/aig/aig_manager.h:109:24: note: remove the '< >' - src/lib/bitblast/aig/aig_manager.h:110:3: warning: template-id not allowed for destructor in C++20 [-Wtemplate-id-cdtor] - 110 | ~BitInterface<AigNode>(); - | ^ - src/lib/bitblast/aig/aig_manager.h:110:3: note: remove the '< >' - (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 check_unsat_core.o -c src/check/check_unsat_core.cpp) - In file included from src/lib/bitblast/aig/aig_cnf.h:13, - from src/solver/bv/bv_bitblast_solver.h:18, - from src/solver/bv/bv_solver.h:15, - from src/solver/solver_engine.h:21, - from src/solving_context.h:23, - from src/check/check_unsat_core.h:16, - from src/check/check_unsat_core.cpp:11: - src/lib/bitblast/aig/aig_manager.h:109:24: warning: template-id not allowed for constructor in C++20 [-Wtemplate-id-cdtor] - 109 | BitInterface<AigNode>(); - | ^ - src/lib/bitblast/aig/aig_manager.h:109:24: note: remove the '< >' - src/lib/bitblast/aig/aig_manager.h:110:3: warning: template-id not allowed for destructor in C++20 [-Wtemplate-id-cdtor] - 110 | ~BitInterface<AigNode>(); - | ^ - src/lib/bitblast/aig/aig_manager.h:110:3: note: remove the '< >' - (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 bv_solver.o -c src/solver/bv/bv_solver.cpp) - In file included from src/lib/bitblast/aig/aig_cnf.h:13, - from src/solver/bv/bv_bitblast_solver.h:18, - from src/solver/bv/bv_solver.h:15, - from src/solver/bv/bv_solver.cpp:11: - src/lib/bitblast/aig/aig_manager.h:109:24: warning: template-id not allowed for constructor in C++20 [-Wtemplate-id-cdtor] - 109 | BitInterface<AigNode>(); - | ^ - src/lib/bitblast/aig/aig_manager.h:109:24: note: remove the '< >' - src/lib/bitblast/aig/aig_manager.h:110:3: warning: template-id not allowed for destructor in C++20 [-Wtemplate-id-cdtor] - 110 | ~BitInterface<AigNode>(); - | ^ - src/lib/bitblast/aig/aig_manager.h:110:3: note: remove the '< >' - (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 check_model.o -c src/check/check_model.cpp) - In file included from src/lib/bitblast/aig/aig_cnf.h:13, - from src/solver/bv/bv_bitblast_solver.h:18, - from src/solver/bv/bv_solver.h:15, - from src/solver/solver_engine.h:21, - from src/solving_context.h:23, - from src/check/check_model.h:16, - from src/check/check_model.cpp:11: - src/lib/bitblast/aig/aig_manager.h:109:24: warning: template-id not allowed for constructor in C++20 [-Wtemplate-id-cdtor] - 109 | BitInterface<AigNode>(); - | ^ - src/lib/bitblast/aig/aig_manager.h:109:24: note: remove the '< >' - src/lib/bitblast/aig/aig_manager.h:110:3: warning: template-id not allowed for destructor in C++20 [-Wtemplate-id-cdtor] - 110 | ~BitInterface<AigNode>(); - | ^ - src/lib/bitblast/aig/aig_manager.h:110:3: note: remove the '< >' - (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) - In file included from src/lib/bitblast/aig/aig_cnf.h:13, - from src/solver/bv/bv_bitblast_solver.h:18, - from src/solver/bv/bv_solver.h:15, - from src/solver/solver_engine.h:21, - from src/solver/solver_engine.cpp:11: - src/lib/bitblast/aig/aig_manager.h:109:24: warning: template-id not allowed for constructor in C++20 [-Wtemplate-id-cdtor] - 109 | BitInterface<AigNode>(); - | ^ - src/lib/bitblast/aig/aig_manager.h:109:24: note: remove the '< >' - src/lib/bitblast/aig/aig_manager.h:110:3: warning: template-id not allowed for destructor in C++20 [-Wtemplate-id-cdtor] - 110 | ~BitInterface<AigNode>(); - | ^ - src/lib/bitblast/aig/aig_manager.h:110:3: note: remove the '< >' - 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 aig_bitblaster.o -c src/solver/bv/aig_bitblaster.cpp) - In file included from src/lib/bitblast/aig_bitblaster.h:14, - from src/solver/bv/aig_bitblaster.h:14, - from src/solver/bv/aig_bitblaster.cpp:11: - src/lib/bitblast/aig/aig_manager.h:109:24: warning: template-id not allowed for constructor in C++20 [-Wtemplate-id-cdtor] - 109 | BitInterface<AigNode>(); - | ^ - src/lib/bitblast/aig/aig_manager.h:109:24: note: remove the '< >' - src/lib/bitblast/aig/aig_manager.h:110:3: warning: template-id not allowed for destructor in C++20 [-Wtemplate-id-cdtor] - 110 | ~BitInterface<AigNode>(); - | ^ - src/lib/bitblast/aig/aig_manager.h:110:3: note: remove the '< >' - (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 preprocessor.o -c src/preprocess/preprocessor.cpp) - In file included from src/lib/bitblast/aig/aig_cnf.h:13, - from src/solver/bv/bv_bitblast_solver.h:18, - from src/solver/bv/bv_solver.h:15, - from src/solver/solver_engine.h:21, - from src/solving_context.h:23, - from src/preprocess/preprocessor.cpp:14: - src/lib/bitblast/aig/aig_manager.h:109:24: warning: template-id not allowed for constructor in C++20 [-Wtemplate-id-cdtor] - 109 | BitInterface<AigNode>(); - | ^ - src/lib/bitblast/aig/aig_manager.h:109:24: note: remove the '< >' - src/lib/bitblast/aig/aig_manager.h:110:3: warning: template-id not allowed for destructor in C++20 [-Wtemplate-id-cdtor] - 110 | ~BitInterface<AigNode>(); - | ^ - src/lib/bitblast/aig/aig_manager.h:110:3: note: remove the '< >' - (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 bv_bitblast_solver.o -c src/solver/bv/bv_bitblast_solver.cpp) - In file included from src/lib/bitblast/aig/aig_cnf.h:13, - from src/solver/bv/bv_bitblast_solver.h:18, - from src/solver/bv/bv_bitblast_solver.cpp:11: - src/lib/bitblast/aig/aig_manager.h:109:24: warning: template-id not allowed for constructor in C++20 [-Wtemplate-id-cdtor] - 109 | BitInterface<AigNode>(); - | ^ - src/lib/bitblast/aig/aig_manager.h:109:24: note: remove the '< >' - src/lib/bitblast/aig/aig_manager.h:110:3: warning: template-id not allowed for destructor in C++20 [-Wtemplate-id-cdtor] - 110 | ~BitInterface<AigNode>(); - | ^ - src/lib/bitblast/aig/aig_manager.h:110:3: note: remove the '< >' - (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 bv_prop_solver.o -c src/solver/bv/bv_prop_solver.cpp) - In file included from src/lib/bitblast/aig/aig_cnf.h:13, - from src/solver/bv/bv_bitblast_solver.h:18, - from src/solver/bv/bv_prop_solver.h:18, - from src/solver/bv/bv_prop_solver.cpp:11: - src/lib/bitblast/aig/aig_manager.h:109:24: warning: template-id not allowed for constructor in C++20 [-Wtemplate-id-cdtor] - 109 | BitInterface<AigNode>(); - | ^ - src/lib/bitblast/aig/aig_manager.h:109:24: note: remove the '< >' - src/lib/bitblast/aig/aig_manager.h:110:3: warning: template-id not allowed for destructor in C++20 [-Wtemplate-id-cdtor] - 110 | ~BitInterface<AigNode>(); - | ^ - src/lib/bitblast/aig/aig_manager.h:110:3: note: remove the '< >' - (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 quant_solver.o -c src/solver/quant/quant_solver.cpp) - In file included from src/lib/bitblast/aig/aig_cnf.h:13, - from src/solver/bv/bv_bitblast_solver.h:18, - from src/solver/bv/bv_solver.h:15, - from src/solver/solver_engine.h:21, - from src/solving_context.h:23, - from src/solver/quant/quant_solver.cpp:18: - src/lib/bitblast/aig/aig_manager.h:109:24: warning: template-id not allowed for constructor in C++20 [-Wtemplate-id-cdtor] - 109 | BitInterface<AigNode>(); - | ^ - src/lib/bitblast/aig/aig_manager.h:109:24: note: remove the '< >' - src/lib/bitblast/aig/aig_manager.h:110:3: warning: template-id not allowed for destructor in C++20 [-Wtemplate-id-cdtor] - 110 | ~BitInterface<AigNode>(); - | ^ - src/lib/bitblast/aig/aig_manager.h:110:3: note: remove the '< >' - (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 solving_context.o -c src/solving_context.cpp) - In file included from src/lib/bitblast/aig/aig_cnf.h:13, - from src/solver/bv/bv_bitblast_solver.h:18, - from src/solver/bv/bv_solver.h:15, - from src/solver/solver_engine.h:21, - from src/solving_context.h:23, - from src/solving_context.cpp:11: - src/lib/bitblast/aig/aig_manager.h:109:24: warning: template-id not allowed for constructor in C++20 [-Wtemplate-id-cdtor] - 109 | BitInterface<AigNode>(); - | ^ - src/lib/bitblast/aig/aig_manager.h:109:24: note: remove the '< >' - src/lib/bitblast/aig/aig_manager.h:110:3: warning: template-id not allowed for destructor in C++20 [-Wtemplate-id-cdtor] - 110 | ~BitInterface<AigNode>(); - | ^ - src/lib/bitblast/aig/aig_manager.h:110:3: note: remove the '< >' - (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(); - | ^~ [ERROR] The compilation of bitwuzla-cxx.0.2.0 failed at "dune build -p bitwuzla-cxx -j 255 @install". build failed...