Build:
- 0
2026-07-14 16:42.55: New job: build bitwuzla-bin.1.0.0 (7a5b39e958a2)
2026-07-14 16:42.55: Waiting for resource in pool day11-builds
2026-07-14 16:55.49: Got resource from pool day11-builds
2026-07-14 16:55.49: [profile full] build bitwuzla-bin.1.0.0
2026-07-14 16:55.49: build bitwuzla-bin.1.0.0 (7a5b39e958a2)
=== DEPENDENCIES (5 transitive) ===
conf-cmake.1 5cf7da35ec4d
conf-g++.1.0 c249686a4f8c
conf-gcc.1.0 2c0a2d801a00
conf-git.1.1 0d0ba4e4d5f7
conf-gmp.5 be8168159001
=== STDOUT ===
Processing: [default: loading data]
[bitwuzla-bin.1.0.0: dl]
[bitwuzla-bin.1.0.0: extract]
-> retrieved bitwuzla-bin.1.0.0 (https://opam.ocaml.org/cache)
[bitwuzla-bin: sh]
+ /usr/bin/sh "-c" "cd vendor/cadical && ./configure -fPIC" (CWD=/home/opam/.opam/default/.opam-switch/build/bitwuzla-bin.1.0.0)
- configure: making default 'build' directory
- configure: building in default '/home/opam/.opam/default/.opam-switch/build/bitwuzla-bin.1.0.0/vendor/cadical/build'
- configure: root directory '/home/opam/.opam/default/.opam-switch/build/bitwuzla-bin.1.0.0/vendor/cadical'
- configure: source directory '/home/opam/.opam/default/.opam-switch/build/bitwuzla-bin.1.0.0/vendor/cadical/src'
- configure: compiler supports all required C99/C++11 extensions
- configure: unlocked IO with '{putc,getc}_unlocked' seems to work
- configure: compiling with 'g++ -Wall -Wextra -O3 -DNDEBUG -fPIC'
- configure: generated 'build/makefile' from '../makefile.in'
- configure: generated '../makefile' as proxy to ...
- configure: ... '/home/opam/.opam/default/.opam-switch/build/bitwuzla-bin.1.0.0/vendor/cadical/build/makefile'
- configure: linking '/home/opam/.opam/default/.opam-switch/build/bitwuzla-bin.1.0.0/vendor/cadical/makefile'
- configure: now run 'make' to compile CaDiCaL
- configure: optionally run 'make test'
[bitwuzla-bin: make 39]
+ /usr/bin/make "-j" "39" "-C" "vendor/cadical/build" (CWD=/home/opam/.opam/default/.opam-switch/build/bitwuzla-bin.1.0.0)
- make: Entering directory '/home/opam/.opam/default/.opam-switch/build/bitwuzla-bin.1.0.0/vendor/cadical/build'
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/analyze.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/arena.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/assume.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/averages.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/backtrack.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/backward.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/bins.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/block.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/ccadical.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/checker.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/clause.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/collect.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/compact.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/condition.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/config.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/contract.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/cover.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/decide.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/decompose.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/deduplicate.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/elim.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/ema.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/extend.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/external.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/file.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/flags.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/format.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/gates.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/instantiate.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/internal.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/ipasir.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/limit.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/logging.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/lookahead.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/lucky.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/message.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/minimize.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/occs.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/options.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/parse.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/phases.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/probe.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/profile.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:49,
- 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).
- | ^~~~~~~~
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/proof.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/propagate.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/queue.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/random.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/reap.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/reduce.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/rephase.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/report.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/resources.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/restart.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/restore.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/score.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/shrink.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/signal.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/solution.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/solver.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/stats.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/subsume.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/terminal.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/ternary.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/tracer.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/transred.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/util.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/var.cpp
- ../scripts/make-build-header.sh > build.hpp
- make-build-header.sh: warning: could not determine 'IDENTIFIER' (git id)
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/vivify.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/walk.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/watch.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/cadical.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/mobical.cpp
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/version.cpp
- ../src/solver.cpp: In destructor 'CaDiCaL::Solver::~Solver()':
- ../src/solver.cpp:259:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare]
- 259 | if ((this == 0)) break; \
- | ^~
- ../src/solver.cpp:346:3: note: in expansion of macro 'TRACE'
- 346 | TRACE ("reset");
- | ^~~~~
- ../src/solver.cpp: In member function 'int CaDiCaL::Solver::vars()':
- ../src/solver.cpp:259:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare]
- 259 | if ((this == 0)) break; \
- | ^~
- ../src/solver.cpp:394:3: note: in expansion of macro 'TRACE'
- 394 | TRACE ("vars");
- | ^~~~~
- ../src/solver.cpp: In member function 'void CaDiCaL::Solver::reserve(int)':
- ../src/solver.cpp:259:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare]
- 259 | if ((this == 0)) break; \
- | ^~
- ../src/solver.cpp:402:3: note: in expansion of macro 'TRACE'
- 402 | TRACE ("reserve", min_max_var);
- | ^~~~~
- ../src/solver.cpp: In member function 'bool CaDiCaL::Solver::set(const char*, int)':
- ../src/solver.cpp:259:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare]
- 259 | if ((this == 0)) break; \
- | ^~
- ../src/solver.cpp:449:3: note: in expansion of macro 'TRACE'
- 449 | TRACE ("set", arg, val);
- | ^~~~~
- ../src/solver.cpp: In member function 'bool CaDiCaL::Solver::limit(const char*, int)':
- ../src/solver.cpp:259:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare]
- 259 | if ((this == 0)) break; \
- | ^~
- ../src/solver.cpp:489:3: note: in expansion of macro 'TRACE'
- 489 | TRACE ("limit", arg, val);
- | ^~~~~
- ../src/solver.cpp: In member function 'void CaDiCaL::Solver::add(int)':
- ../src/solver.cpp:259:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare]
- 259 | if ((this == 0)) break; \
- | ^~
- ../src/solver.cpp:524:3: note: in expansion of macro 'TRACE'
- 524 | TRACE ("add", lit);
- | ^~~~~
- ../src/solver.cpp: In member function 'void CaDiCaL::Solver::assume(int)':
- ../src/solver.cpp:259:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare]
- 259 | if ((this == 0)) break; \
- | ^~
- ../src/solver.cpp:535:3: note: in expansion of macro 'TRACE'
- 535 | TRACE ("assume", lit);
- | ^~~~~
- ../src/solver.cpp: In member function 'int CaDiCaL::Solver::lookahead()':
- ../src/solver.cpp:259:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare]
- 259 | if ((this == 0)) break; \
- | ^~
- ../src/solver.cpp:547:3: note: in expansion of macro 'TRACE'
- 547 | TRACE ("lookahead");
- | ^~~~~
- ../src/solver.cpp:259:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare]
- 259 | if ((this == 0)) break; \
- | ^~
- ../src/solver.cpp:544:3: note: in expansion of macro 'TRACE'
- 544 | TRACE ("lookahead");
- | ^~~~~
- ../src/solver.cpp: In member function 'void CaDiCaL::Solver::reset_assumptions()':
- ../src/solver.cpp:259:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare]
- 259 | if ((this == 0)) break; \
- | ^~
- ../src/solver.cpp:564:3: note: in expansion of macro 'TRACE'
- 564 | TRACE ("reset_assumptions");
- | ^~~~~
- ../src/solver.cpp: In member function 'int CaDiCaL::Solver::solve()':
- ../src/solver.cpp:259:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare]
- 259 | if ((this == 0)) break; \
- | ^~
- ../src/solver.cpp:605:3: note: in expansion of macro 'TRACE'
- 605 | TRACE ("solve");
- | ^~~~~
- ../src/solver.cpp: In member function 'int CaDiCaL::Solver::simplify(int)':
- ../src/solver.cpp:259:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare]
- 259 | if ((this == 0)) break; \
- | ^~
- ../src/solver.cpp:613:3: note: in expansion of macro 'TRACE'
- 613 | TRACE ("simplify", rounds);
- | ^~~~~
- ../src/solver.cpp: In member function 'bool CaDiCaL::Solver::failed(int)':
- ../src/solver.cpp:259:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare]
- 259 | if ((this == 0)) break; \
- | ^~
- ../src/solver.cpp:637:3: note: in expansion of macro 'TRACE'
- 637 | TRACE ("failed", lit);
- | ^~~~~
- ../src/solver.cpp: In member function 'void CaDiCaL::Solver::phase(int)':
- ../src/solver.cpp:259:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare]
- 259 | if ((this == 0)) break; \
- | ^~
- ../src/solver.cpp:657:3: note: in expansion of macro 'TRACE'
- 657 | TRACE ("phase", lit);
- | ^~~~~
- ../src/solver.cpp: In member function 'void CaDiCaL::Solver::unphase(int)':
- ../src/solver.cpp:259:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare]
- 259 | if ((this == 0)) break; \
- | ^~
- ../src/solver.cpp:665:3: note: in expansion of macro 'TRACE'
- 665 | TRACE ("unphase", lit);
- | ^~~~~
- ../src/solver.cpp: In member function 'int CaDiCaL::Solver::active() const':
- ../src/solver.cpp:259:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare]
- 259 | if ((this == 0)) break; \
- | ^~
- ../src/solver.cpp:740:3: note: in expansion of macro 'TRACE'
- 740 | TRACE ("active");
- | ^~~~~
- ../src/solver.cpp: In member function 'int64_t CaDiCaL::Solver::redundant() const':
- ../src/solver.cpp:259:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare]
- 259 | if ((this == 0)) break; \
- | ^~
- ../src/solver.cpp:748:3: note: in expansion of macro 'TRACE'
- 748 | TRACE ("redundant");
- | ^~~~~
- ../src/solver.cpp: In member function 'int64_t CaDiCaL::Solver::irredundant() const':
- ../src/solver.cpp:259:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare]
- 259 | if ((this == 0)) break; \
- | ^~
- ../src/solver.cpp:756:3: note: in expansion of macro 'TRACE'
- 756 | TRACE ("irredundant");
- | ^~~~~
- ../src/solver.cpp: In member function 'void CaDiCaL::Solver::freeze(int)':
- ../src/solver.cpp:259:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare]
- 259 | if ((this == 0)) break; \
- | ^~
- ../src/solver.cpp:766:3: note: in expansion of macro 'TRACE'
- 766 | TRACE ("freeze", lit);
- | ^~~~~
- ../src/solver.cpp: In member function 'void CaDiCaL::Solver::statistics()':
- ../src/solver.cpp:259:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare]
- 259 | if ((this == 0)) break; \
- | ^~
- ../src/solver.cpp:911:3: note: in expansion of macro 'TRACE'
- 911 | TRACE ("stats");
- | ^~~~~
- ../src/solver.cpp: In member function 'void CaDiCaL::Solver::resources()':
- ../src/solver.cpp:259:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare]
- 259 | if ((this == 0)) break; \
- | ^~
- ../src/solver.cpp:919:3: note: in expansion of macro 'TRACE'
- 919 | TRACE ("resources");
- | ^~~~~
- ../src/solver.cpp: In member function 'void CaDiCaL::Solver::dump_cnf()':
- ../src/solver.cpp:259:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare]
- 259 | if ((this == 0)) break; \
- | ^~
- ../src/solver.cpp:1023:3: note: in expansion of macro 'TRACE'
- 1023 | TRACE ("dump");
- | ^~~~~
- ../src/solver.cpp: In constructor 'CaDiCaL::Solver::Solver()':
- ../src/solver.cpp:259:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare]
- 259 | if ((this == 0)) break; \
- | ^~
- ../src/solver.cpp:335:3: note: in expansion of macro 'TRACE'
- 335 | TRACE ("init");
- | ^~~~~
- ../src/solver.cpp: In member function 'void CaDiCaL::Solver::melt(int)':
- ../src/solver.cpp:259:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare]
- 259 | if ((this == 0)) break; \
- | ^~
- ../src/solver.cpp:774:3: note: in expansion of macro 'TRACE'
- 774 | TRACE ("melt", lit);
- | ^~~~~
- ../src/solver.cpp: In member function 'bool CaDiCaL::Solver::frozen(int) const':
- ../src/solver.cpp:259:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare]
- 259 | if ((this == 0)) break; \
- | ^~
- ../src/solver.cpp:784:3: note: in expansion of macro 'TRACE'
- 784 | TRACE ("frozen", lit);
- | ^~~~~
- ../src/solver.cpp: In member function 'int CaDiCaL::Solver::fixed(int) const':
- ../src/solver.cpp:259:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare]
- 259 | if ((this == 0)) break; \
- | ^~
- ../src/solver.cpp:648:3: note: in expansion of macro 'TRACE'
- 648 | TRACE ("fixed", lit);
- | ^~~~~
- ../src/solver.cpp: In member function 'int CaDiCaL::Solver::val(int)':
- ../src/solver.cpp:259:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare]
- 259 | if ((this == 0)) break; \
- | ^~
- ../src/solver.cpp:626:3: note: in expansion of macro 'TRACE'
- 626 | TRACE ("val", lit);
- | ^~~~~
- ../src/solver.cpp: In member function 'CaDiCaL::Solver::CubesWithStatus CaDiCaL::Solver::generate_cubes(int, int)':
- ../src/solver.cpp:259:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare]
- 259 | if ((this == 0)) break; \
- | ^~
- ../src/solver.cpp:555:3: note: in expansion of macro 'TRACE'
- 555 | TRACE ("lookahead_cubes");
- | ^~~~~
- ../src/solver.cpp:259:3: warning: 'nonnull' argument 'this' compared to NULL [-Wnonnull-compare]
- 259 | if ((this == 0)) break; \
- | ^~
- ../src/solver.cpp:552:3: note: in expansion of macro 'TRACE'
- 552 | TRACE ("lookahead_cubes");
- | ^~~~~
- ar rc libcadical.a analyze.o arena.o assume.o averages.o backtrack.o backward.o bins.o block.o ccadical.o checker.o clause.o collect.o compact.o condition.o config.o contract.o cover.o decide.o decompose.o deduplicate.o elim.o ema.o extend.o external.o file.o flags.o format.o gates.o instantiate.o internal.o ipasir.o limit.o logging.o lookahead.o lucky.o message.o minimize.o occs.o options.o parse.o phases.o probe.o profile.o proof.o propagate.o queue.o random.o reap.o reduce.o rephase.o report.o resources.o restart.o restore.o score.o shrink.o signal.o solution.o solver.o stats.o subsume.o terminal.o ternary.o tracer.o transred.o util.o var.o version.o vivify.o walk.o watch.o
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -o cadical cadical.o -L. -lcadical
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -o mobical mobical.o -L. -lcadical
- make: Leaving directory '/home/opam/.opam/default/.opam-switch/build/bitwuzla-bin.1.0.0/vendor/cadical/build'
[bitwuzla-bin: sh]
+ /usr/bin/sh "-c" "cd vendor/btor2tools && ./configure.sh" (CWD=/home/opam/.opam/default/.opam-switch/build/bitwuzla-bin.1.0.0)
- CMake Deprecation Warning at CMakeLists.txt:1 (cmake_minimum_required):
- Compatibility with CMake < 3.10 will be removed from a future version of
- CMake.
-
- Update the VERSION argument <min> value. Or, use the <min>...<max> syntax
- to tell CMake that the project requires at least <min> but has been updated
- to work with policies introduced by <max> or earlier.
-
-
- -- The C compiler identification is GNU 14.2.0
- -- The CXX compiler identification is GNU 14.2.0
- -- Detecting C compiler ABI info
- -- Detecting C compiler ABI info - done
- -- Check for working C compiler: /usr/bin/cc - skipped
- -- Detecting C compile features
- -- Detecting C compile features - done
- -- Detecting CXX compiler ABI info
- -- Detecting CXX compiler ABI info - done
- -- Check for working CXX compiler: /usr/bin/c++ - skipped
- -- Detecting CXX compile features
- -- Detecting CXX compile features - done
- -- Performing Test HAVE_FLAG_W
- -- Performing Test HAVE_FLAG_W - Success
- -- Configuring with C flag '-W'
- -- Configuring with CXX flag '-W'
- -- Performing Test HAVE_FLAG_Wall
- -- Performing Test HAVE_FLAG_Wall - Success
- -- Configuring with C flag '-Wall'
- -- Configuring with CXX flag '-Wall'
- -- Performing Test HAVE_FLAG_Wextra
- -- Performing Test HAVE_FLAG_Wextra - Success
- -- Configuring with C flag '-Wextra'
- -- Configuring with CXX flag '-Wextra'
- -- Performing Test HAVE_FLAG_Wredundant_decls
- -- Performing Test HAVE_FLAG_Wredundant_decls - Success
- -- Configuring with C flag '-Wredundant-decls'
- -- Configuring with CXX flag '-Wredundant-decls'
- -- Performing Test HAVE_FLAG_std_gnu99
- -- Performing Test HAVE_FLAG_std_gnu99 - Success
- -- Configuring with C flag '-std=gnu99'
- -- Configuring with CXX flag '-std=gnu++11'
- -- Performing Test HAVE_FLAG_O3
- -- Performing Test HAVE_FLAG_O3 - Success
- -- Configuring with C flag '-O3'
- -- Configuring with CXX flag '-O3'
- -- Performing Test HAVE_FLAG_DNDEBUG
- -- Performing Test HAVE_FLAG_DNDEBUG - Success
- -- Configuring with C flag '-DNDEBUG'
- -- Configuring with CXX flag '-DNDEBUG'
- -- Configuring done (2.4s)
- -- Generating done (0.0s)
- -- Build files have been written to: /home/opam/.opam/default/.opam-switch/build/bitwuzla-bin.1.0.0/vendor/btor2tools/build
[bitwuzla-bin: make 39]
+ /usr/bin/make "-j" "39" "-C" "vendor/btor2tools/build" (CWD=/home/opam/.opam/default/.opam-switch/build/bitwuzla-bin.1.0.0)
- make: Entering directory '/home/opam/.opam/default/.opam-switch/build/bitwuzla-bin.1.0.0/vendor/btor2tools/build'
- [ 7%] Building CXX object src/CMakeFiles/btorsplit.dir/btorsplit.cpp.o
- [ 14%] Building C object src/CMakeFiles/btor2parser.dir/btor2parser/btor2parser.c.o
- /home/opam/.opam/default/.opam-switch/build/bitwuzla-bin.1.0.0/vendor/btor2tools/src/btorsplit.cpp:25:8: error: 'uint32_t' does not name a type
- 25 | static uint32_t s_verbosity = 0;
- | ^~~~~~~~
- /home/opam/.opam/default/.opam-switch/build/bitwuzla-bin.1.0.0/vendor/btor2tools/src/btorsplit.cpp:22:1: note: 'uint32_t' is defined in header '<cstdint>'; this is probably fixable by adding '#include <cstdint>'
- 21 | #include <vector>
- +++ |+#include <cstdint>
- 22 |
- /home/opam/.opam/default/.opam-switch/build/bitwuzla-bin.1.0.0/vendor/btor2tools/src/btorsplit.cpp: In function 'void split_file(std::string, bool)':
- /home/opam/.opam/default/.opam-switch/build/bitwuzla-bin.1.0.0/vendor/btor2tools/src/btorsplit.cpp:97:7: error: 's_verbosity' was not declared in this scope
- 97 | if (s_verbosity)
- | ^~~~~~~~~~~
- /home/opam/.opam/default/.opam-switch/build/bitwuzla-bin.1.0.0/vendor/btor2tools/src/btorsplit.cpp:103:3: error: 'uint32_t' was not declared in this scope
- 103 | uint32_t ndigits = 0;
- | ^~~~~~~~
- /home/opam/.opam/default/.opam-switch/build/bitwuzla-bin.1.0.0/vendor/btor2tools/src/btorsplit.cpp:103:3: note: 'uint32_t' is defined in header '<cstdint>'; this is probably fixable by adding '#include <cstdint>'
- /home/opam/.opam/default/.opam-switch/build/bitwuzla-bin.1.0.0/vendor/btor2tools/src/btorsplit.cpp:105:52: error: 'ndigits' was not declared in this scope
- 105 | for (size_t i = bad.size(); i > 0; i = i / 10, ++ndigits)
- | ^~~~~~~
- /home/opam/.opam/default/.opam-switch/build/bitwuzla-bin.1.0.0/vendor/btor2tools/src/btorsplit.cpp:112:60: error: 'ndigits' was not declared in this scope
- 112 | ss << prefix << "-p" << std::setfill('0') << std::setw(ndigits) << num_prop
- | ^~~~~~~
- /home/opam/.opam/default/.opam-switch/build/bitwuzla-bin.1.0.0/vendor/btor2tools/src/btorsplit.cpp:133:9: error: 's_verbosity' was not declared in this scope
- 133 | if (s_verbosity) std::cout << "Generated " << ss.str() << std::endl;
- | ^~~~~~~~~~~
- /home/opam/.opam/default/.opam-switch/build/bitwuzla-bin.1.0.0/vendor/btor2tools/src/btorsplit.cpp: In function 'int main(int, char**)':
- /home/opam/.opam/default/.opam-switch/build/bitwuzla-bin.1.0.0/vendor/btor2tools/src/btorsplit.cpp:147:9: error: 's_verbosity' was not declared in this scope
- 147 | ++s_verbosity;
- | ^~~~~~~~~~~
- /home/opam/.opam/default/.opam-switch/build/bitwuzla-bin.1.0.0/vendor/btor2tools/src/btorsplit.cpp:171:9: error: 's_verbosity' was not declared in this scope
- 171 | if (s_verbosity) std::cout << "Processing " << infile << std::endl;
- | ^~~~~~~~~~~
- make[2]: *** [src/CMakeFiles/btorsplit.dir/build.make:79: src/CMakeFiles/btorsplit.dir/btorsplit.cpp.o] Error 1
- make[1]: *** [CMakeFiles/Makefile2:211: src/CMakeFiles/btorsplit.dir/all] Error 2
- make[1]: *** Waiting for unfinished jobs....
- [ 21%] Linking C shared library ../lib/libbtor2parser.so
- [ 21%] Built target btor2parser
- make: *** [Makefile:136: all] Error 2
- make: Leaving directory '/home/opam/.opam/default/.opam-switch/build/bitwuzla-bin.1.0.0/vendor/btor2tools/build'
[ERROR] The compilation of bitwuzla-bin.1.0.0 failed at "make -j 39 -C vendor/btor2tools/build".
build failed...
=== STDERR ===
2026-07-14 16:58.21: FAILED: build bitwuzla-bin.1.0.0
2026-07-14 16:58.21: Job failed: build failed: bitwuzla-bin.1.0.0