Building on doris.caelum.ci.dev
day10 dispatch:
verb : health-check
opam-repository : <default>
opam-repo commit : ae6f88cbf223d078928da4d89e303253ea5df2f0
mirror : /var/cache/obuilder/ocluster/git/opam-repository.git-b322f7b18d276db68487afc3dfc5a5befdd45818
cache-dir : /var/cache/day10
ocaml-version : ocaml.5.4.1
package : bitwuzla-bin.1.0.0
os-distribution : debian
os-version : 13
with-test : false
+ 'day10' 'health-check' '--cache-dir' '/var/cache/day10' '--log' '--opam-repository' '/var/cache/obuilder/ocluster/git/opam-repository.git-b322f7b18d276db68487afc3dfc5a5befdd45818:ae6f88cbf223d078928da4d89e303253ea5df2f0' '--ocaml-version' 'ocaml.5.4.1' '--arch' 'x86_64' '--os' 'linux' '--os-distribution' 'debian' '--os-version' '13' 'bitwuzla-bin.1.0.0'
digraph opam {
"bitwuzla-bin.1.0.0" -> {"conf-cmake.1" "conf-g++.1.0" "conf-gcc.1.0" "conf-git.1.1" "conf-gmp.5"}
}
Processing: [default: loading data]
The following system packages will first need to be installed:
cmake
<><> Handling external dependencies <><><><><><><><><><><><><><><><><><><><><><>
+ /usr/bin/sudo "apt-get" "install" "-qq" "-yy" "cmake"
- Selecting previously unselected package cmake-data.
- (Reading database ...
(Reading database ... 5%
(Reading database ... 10%
(Reading database ... 15%
(Reading database ... 20%
(Reading database ... 25%
(Reading database ... 30%
(Reading database ... 35%
(Reading database ... 40%
(Reading database ... 45%
(Reading database ... 50%
(Reading database ... 55%
(Reading database ... 60%
(Reading database ... 65%
(Reading database ... 70%
(Reading database ... 75%
(Reading database ... 80%
(Reading database ... 85%
(Reading database ... 90%
(Reading database ... 95%
(Reading database ... 100%
(Reading database ... 20108 files and directories currently installed.)
- Preparing to unpack .../0-cmake-data_3.31.6-2_all.deb ...
- Unpacking cmake-data (3.31.6-2) ...
- Selecting previously unselected package libxml2:amd64.
- Preparing to unpack .../1-libxml2_2.12.7+dfsg+really2.9.14-2.1+deb13u3_amd64.deb ...
- Unpacking libxml2:amd64 (2.12.7+dfsg+really2.9.14-2.1+deb13u3) ...
- Selecting previously unselected package libarchive13t64:amd64.
- Preparing to unpack .../2-libarchive13t64_3.7.4-4+deb13u1_amd64.deb ...
- Unpacking libarchive13t64:amd64 (3.7.4-4+deb13u1) ...
- Selecting previously unselected package libjsoncpp26:amd64.
- Preparing to unpack .../3-libjsoncpp26_1.9.6-3_amd64.deb ...
- Unpacking libjsoncpp26:amd64 (1.9.6-3) ...
- Selecting previously unselected package librhash1:amd64.
- Preparing to unpack .../4-librhash1_1.4.5-1_amd64.deb ...
- Unpacking librhash1:amd64 (1.4.5-1) ...
- Selecting previously unselected package libuv1t64:amd64.
- Preparing to unpack .../5-libuv1t64_1.50.0-2_amd64.deb ...
- Unpacking libuv1t64:amd64 (1.50.0-2) ...
- Selecting previously unselected package cmake.
- Preparing to unpack .../6-cmake_3.31.6-2_amd64.deb ...
- Unpacking cmake (3.31.6-2) ...
- Setting up libuv1t64:amd64 (1.50.0-2) ...
- Setting up libjsoncpp26:amd64 (1.9.6-3) ...
- Setting up cmake-data (3.31.6-2) ...
- Setting up librhash1:amd64 (1.4.5-1) ...
- Setting up libxml2:amd64 (2.12.7+dfsg+really2.9.14-2.1+deb13u3) ...
- Setting up libarchive13t64:amd64 (3.7.4-4+deb13u1) ...
- Setting up cmake (3.31.6-2) ...
- Processing triggers for libc-bin (2.41-12+deb13u3) ...
[conf-cmake.1/configure.sh: dl]
-> retrieved conf-cmake.1 (https://raw.githubusercontent.com/ocaml/opam-source-archives/main/patches/conf-cmake/configure.sh)
[conf-cmake: sh configure.sh]
+ /usr/bin/sh "-ex" "configure.sh" (CWD=/home/opam/.opam/default/.opam-switch/build/conf-cmake.1)
- + command -v cmake3
- + command -v cmake
- /usr/bin/cmake
- + cmake_cmd=cmake
- + echo cmd: "cmake"
-> compiled conf-cmake.1
-> installed conf-cmake.1
Processing: [default: loading data]
[conf-g++: g++]
+ /usr/bin/g++ "--version" (CWD=/home/opam/.opam/default/.opam-switch/build/conf-g++.1.0)
- g++ (Debian 14.2.0-19) 14.2.0
- Copyright (C) 2024 Free Software Foundation, Inc.
- This is free software; see the source for copying conditions. There is NO
- warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
-
-> compiled conf-g++.1.0
-> installed conf-g++.1.0
Processing: [default: loading data]
[conf-gcc: gcc]
+ /usr/bin/gcc "--version" (CWD=/home/opam/.opam/default/.opam-switch/build/conf-gcc.1.0)
- gcc (Debian 14.2.0-19) 14.2.0
- Copyright (C) 2024 Free Software Foundation, Inc.
- This is free software; see the source for copying conditions. There is NO
- warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
-
-> compiled conf-gcc.1.0
-> installed conf-gcc.1.0
Processing: [default: loading data]
[conf-git: git]
+ /usr/bin/git "--version" (CWD=/home/opam/.opam/default/.opam-switch/build/conf-git.1.1)
- git version 2.47.3
-> compiled conf-git.1.1
-> installed conf-git.1.1
Processing: [default: loading data]
The following system packages will first need to be installed:
libgmp-dev
<><> Handling external dependencies <><><><><><><><><><><><><><><><><><><><><><>
+ /usr/bin/sudo "apt-get" "install" "-qq" "-yy" "libgmp-dev"
- Selecting previously unselected package libgmpxx4ldbl:amd64.
- (Reading database ...
(Reading database ... 5%
(Reading database ... 10%
(Reading database ... 15%
(Reading database ... 20%
(Reading database ... 25%
(Reading database ... 30%
(Reading database ... 35%
(Reading database ... 40%
(Reading database ... 45%
(Reading database ... 50%
(Reading database ... 55%
(Reading database ... 60%
(Reading database ... 65%
(Reading database ... 70%
(Reading database ... 75%
(Reading database ... 80%
(Reading database ... 85%
(Reading database ... 90%
(Reading database ... 95%
(Reading database ... 100%
(Reading database ... 20108 files and directories currently installed.)
- Preparing to unpack .../libgmpxx4ldbl_2%3a6.3.0+dfsg-3_amd64.deb ...
- Unpacking libgmpxx4ldbl:amd64 (2:6.3.0+dfsg-3) ...
- Selecting previously unselected package libgmp-dev:amd64.
- Preparing to unpack .../libgmp-dev_2%3a6.3.0+dfsg-3_amd64.deb ...
- Unpacking libgmp-dev:amd64 (2:6.3.0+dfsg-3) ...
- Setting up libgmpxx4ldbl:amd64 (2:6.3.0+dfsg-3) ...
- Setting up libgmp-dev:amd64 (2:6.3.0+dfsg-3) ...
- Processing triggers for libc-bin (2.41-12+deb13u3) ...
[conf-gmp.5/test.c: dl]
-> retrieved conf-gmp.5 (https://raw.githubusercontent.com/ocaml/opam-source-archives/main/patches/conf-gmp/test.c.4)
[conf-gmp: sh]
+ /usr/bin/sh "-c" "pkg-config --print-errors --exists gmp || cc -c $CFLAGS -I/usr/local/include test.c" (CWD=/home/opam/.opam/default/.opam-switch/build/conf-gmp.5)
- /usr/bin/sh: 1: pkg-config: not found
-> compiled conf-gmp.5
-> installed conf-gmp.5
Processing: [default: loading data]
[bitwuzla-bin.1.0.0: http]
[bitwuzla-bin.1.0.0: extract]
-> retrieved bitwuzla-bin.1.0.0 (https://github.com/bitwuzla/ocaml-bitwuzla/releases/download/1.0.0/bitwuzla-1.0.0.tbz)
[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 255]
+ /usr/bin/make "-j" "255" "-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
- 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
- g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/vivify.cpp
- make-build-header.sh: warning: could not determine 'IDENTIFIER' (git id)
- 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/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).
- | ^~~~~~~~
- ../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 (1.6s)
- -- 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 255]
+ /usr/bin/make "-j" "255" "-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 C object src/CMakeFiles/btor2parser.dir/btor2parser/btor2parser.c.o
- [ 14%] Building CXX object src/CMakeFiles/btorsplit.dir/btorsplit.cpp.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 255 -C vendor/btor2tools/build".
build failed...
[ERROR] failure
Job succeeded
Home|Differences with the last checks|Previous runs