Build:
- 0
2026-07-26 11:14.47: New job: build bitwuzla-cxx.0.3.0 (d6545d3d8b2a)
2026-07-26 11:14.47: Waiting for resource in pool day11-builds
2026-07-26 12:49.37: Got resource from pool day11-builds
2026-07-26 12:49.37: [profile full] build bitwuzla-cxx.0.3.0
2026-07-26 12:49.37: build bitwuzla-cxx.0.3.0 (d6545d3d8b2a)
=== DEPENDENCIES (13 transitive) ===
base-threads.base afe16a8e71c3
base-unix.base 73c0a5fdd34a
conf-g++.1.0 c249686a4f8c
conf-gcc.1.0 2c0a2d801a00
conf-git.1.1 0d0ba4e4d5f7
conf-gmp.5 be8168159001
conf-pkg-config.5 2c611009363a
dune.3.24.1 b9e5a15ad12e
ocaml.4.14.4 ff640eef2ca4
ocaml-base-compiler.4.14.4 0ab775b44d12
ocaml-config.2 3a0479a5d208
ocamlfind.1.9.8 aea9878e34cf
zarith.1.14 3bf0fc9b7912
=== STDOUT ===
Processing: [default: loading data]
[bitwuzla-cxx.0.3.0: dl]
[bitwuzla-cxx.0.3.0: extract]
-> retrieved bitwuzla-cxx.0.3.0 (https://opam.ocaml.org/cache)
[bitwuzla-cxx: dune build]
+ /home/opam/.opam/default/bin/dune "build" "-p" "bitwuzla-cxx" "-j" "39" "@install" (CWD=/home/opam/.opam/default/.opam-switch/build/bitwuzla-cxx.0.3.0)
- (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/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
- Hunk #1 succeeded at 287 (offset 9 lines).
- (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
- 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/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_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_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/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/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/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 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 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 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 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 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 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 '< >'
- (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 '< >'
build failed...
[ERROR] The compilation of bitwuzla-cxx.0.3.0 failed at "dune build -p bitwuzla-cxx -j 39 @install".
=== STDERR ===
2026-07-26 12:54.50: FAILED: build bitwuzla-cxx.0.3.0
2026-07-26 12:54.50: Job failed: build failed: bitwuzla-cxx.0.3.0