Build:
- 0
2026-07-26 10:52.28: New job: build cvc5.1.3.0-2 (6d45520e29c5)
2026-07-26 10:52.28: [profile full] build cvc5.1.3.0-2
2026-07-26 10:52.31: build cvc5.1.3.0-2 (6d45520e29c5)
=== DEPENDENCIES (15 transitive) ===
base-threads.base afe16a8e71c3
base-unix.base 73c0a5fdd34a
compiler-cloning.enabled 22a431860256
conf-cmake.1 5cf7da35ec4d
conf-g++.1.0 c249686a4f8c
conf-gcc.1.0 2c0a2d801a00
conf-gmp.5 be8168159001
conf-python-3.9.0.0 10e92bdeecd9
conf-python-3-dev.1 45c0502fee82
conf-python3-pyparsing.1 a55c6b63bb5d
conf-python3-tomli.1 1d2633443342
dune.3.24.1 0d2a3ba8bfb9
ocaml.5.5.0 af24caade1d3
ocaml-base-compiler.5.5.0 5f93989ce6d7
ocaml-compiler.5.5.0 15edcf5138e5
=== STDOUT ===
Processing: [default: loading data]
[cvc5.1.3.0-2: dl]
[cvc5.1.3.0-2: extract]
-> retrieved cvc5.1.3.0-2 (https://opam.ocaml.org/cache)
[cvc5: dune build]
+ /home/opam/.opam/default/bin/dune "build" "-p" "cvc5" "-j" "39" "@install" (CWD=/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-2)
- (cd _build/default/vendor/cadical && /usr/bin/bash -e -u -o pipefail -c 'CXXFLAGS=-fPIC ./configure')
- configure: making default 'build' directory
- configure: building in default '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-2/_build/default/vendor/cadical/build'
- configure: root directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-2/_build/default/vendor/cadical'
- configure: source directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-2/_build/default/vendor/cadical/src'
- configure: compiler supports all required C99/C++11 extensions
- configure: compiler configuration supports flexible array members
- configure: unlocked IO with '{putc,getc}_unlocked' seems to work
- configure: 'closefrom' seems to be working
- configure: compiling with 'g++ -fPIC -Wall -Wextra -O3 -DNDEBUG'
- configure: generated 'build/makefile' from '../makefile.in'
- configure: generated '../makefile' as proxy to ...
- configure: ... '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-2/_build/default/vendor/cadical/build/makefile'
- configure: linking '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-2/_build/default/vendor/cadical/makefile'
- configure: now run 'make' to compile CaDiCaL
- configure: optionally run 'make test'
- (cd _build/default/vendor/cadical && /usr/bin/bash -e -u -o pipefail -c 'make -j $(opam var jobs)')
- make -C "/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-2/_build/default/vendor/cadical/build"
- make[1]: Entering directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-2/_build/default/vendor/cadical/build'
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/analyze.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/arena.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/assume.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/averages.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/backtrack.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/backward.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/bins.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/block.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/ccadical.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/checker.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/clause.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/collect.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/compact.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/condition.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/config.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/constrain.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/contract.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/cover.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/decide.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/decompose.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/deduplicate.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/drattracer.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/elim.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/ema.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/extend.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/external.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/external_propagate.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/file.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/flags.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/flip.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/format.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/frattracer.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/gates.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/idruptracer.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/instantiate.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/internal.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/ipasir.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/lidruptracer.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/limit.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/logging.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/lookahead.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/lratbuilder.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/lratchecker.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/lrattracer.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/lucky.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/message.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/minimize.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/occs.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/options.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/parse.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/phases.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/probe.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/profile.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/proof.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/propagate.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/queue.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/random.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/reap.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/reduce.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/rephase.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/report.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/resources.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/restart.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/restore.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/score.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/shrink.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/signal.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/solution.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/solver.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/stats.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/subsume.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/terminal.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/ternary.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/transred.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/util.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/var.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/veripbtracer.cpp
- ../scripts/make-build-header.sh > build.hpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/vivify.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/walk.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/watch.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../contrib/craigtracer.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/cadical.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/mobical.cpp
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -c ../src/version.cpp
- 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 constrain.o contract.o cover.o decide.o decompose.o deduplicate.o drattracer.o elim.o ema.o extend.o external.o external_propagate.o file.o flags.o flip.o format.o frattracer.o gates.o idruptracer.o instantiate.o internal.o ipasir.o lidruptracer.o limit.o logging.o lookahead.o lratbuilder.o lratchecker.o lrattracer.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 transred.o util.o var.o veripbtracer.o version.o vivify.o walk.o watch.o craigtracer.o
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -o cadical cadical.o -L. -lcadical
- g++ -fPIC -Wall -Wextra -O3 -DNDEBUG -I../build -I../src -o mobical mobical.o -L. -lcadical
- make[1]: Leaving directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-2/_build/default/vendor/cadical/build'
- make-build-header.sh: warning: could not determine 'IDENTIFIER' (git id)
- (cd _build/default/vendor/libpoly && /usr/bin/cmake -B build -DCMAKE_BUILD_TYPE=$type -DCMAKE_POSITION_INDEPENDENT_CODE=ON -DCMAKE_INSTALL_PREFIX=$prefix)
- -- 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
- -- GMP headers: /usr/include/x86_64-linux-gnu
- -- GMP library: /usr/lib/x86_64-linux-gnu/libgmp.so
- -- Looking for open_memstream
- -- Looking for open_memstream - found
- -- Found PythonInterp: /usr/bin/python3 (found version "3.13.5")
- -- Found PythonLibs: /usr/lib/x86_64-linux-gnu/libpython3.13.so (found version "3.13.5")
- -- Configuring done (1.7s)
- -- Generating done (0.2s)
- -- Build files have been written to: /home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-2/_build/default/vendor/libpoly/build
- 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.
-
-
- CMake Warning (dev) at CMakeLists.txt:72 (find_package):
- Policy CMP0148 is not set: The FindPythonInterp and FindPythonLibs modules
- are removed. Run "cmake --help-policy CMP0148" for policy details. Use
- the cmake_policy command to set the policy and suppress this warning.
-
- This warning is for project developers. Use -Wno-dev to suppress it.
-
- CMake Warning (dev) at python/CMakeLists.txt:16 (find_package):
- Policy CMP0148 is not set: The FindPythonInterp and FindPythonLibs modules
- are removed. Run "cmake --help-policy CMP0148" for policy details. Use
- the cmake_policy command to set the policy and suppress this warning.
-
- This warning is for project developers. Use -Wno-dev to suppress it.
-
- (cd _build/default/vendor/libpoly/build && /usr/bin/bash -e -u -o pipefail -c 'make -j $(opam var jobs)')
- [ 0%] Building C object src/CMakeFiles/poly.dir/utils/debug_trace.c.o
- [ 1%] Building C object src/CMakeFiles/static_poly.dir/utils/assignment.c.o
- [ 1%] Building C object src/CMakeFiles/static_poly.dir/utils/debug_trace.c.o
- [ 1%] Building C object src/CMakeFiles/static_pic_poly.dir/utils/debug_trace.c.o
- [ 1%] Building C object src/CMakeFiles/static_pic_poly.dir/utils/assignment.c.o
- [ 1%] Building C object src/CMakeFiles/static_poly.dir/utils/statistics.c.o
- [ 1%] Building C object src/CMakeFiles/static_poly.dir/utils/output.c.o
- [ 1%] Building C object src/CMakeFiles/poly.dir/utils/assignment.c.o
- [ 2%] Building C object src/CMakeFiles/static_pic_poly.dir/utils/statistics.c.o
- [ 3%] Building C object src/CMakeFiles/static_poly.dir/utils/sign_condition.c.o
- [ 3%] Building C object src/CMakeFiles/static_poly.dir/utils/u_memstream.c.o
- [ 3%] Building C object src/CMakeFiles/static_pic_poly.dir/utils/output.c.o
- [ 4%] Building C object src/CMakeFiles/static_poly.dir/number/integer.c.o
- [ 4%] Building C object src/CMakeFiles/static_poly.dir/number/rational.c.o
- [ 5%] Building C object src/CMakeFiles/poly.dir/utils/statistics.c.o
- [ 6%] Building C object src/CMakeFiles/static_pic_poly.dir/utils/sign_condition.c.o
- [ 6%] Building C object src/CMakeFiles/poly.dir/utils/output.c.o
- [ 6%] Building C object src/CMakeFiles/static_pic_poly.dir/utils/u_memstream.c.o
- [ 7%] Building C object src/CMakeFiles/poly.dir/utils/sign_condition.c.o
- [ 8%] Building C object src/CMakeFiles/static_poly.dir/number/dyadic_rational.c.o
- [ 9%] Building C object src/CMakeFiles/static_pic_poly.dir/number/integer.c.o
- [ 9%] Building C object src/CMakeFiles/poly.dir/utils/u_memstream.c.o
- [ 10%] Building C object src/CMakeFiles/poly.dir/number/integer.c.o
- [ 10%] Building C object src/CMakeFiles/poly.dir/number/rational.c.o
- [ 10%] Building C object src/CMakeFiles/static_pic_poly.dir/number/rational.c.o
- [ 10%] Building C object src/CMakeFiles/static_poly.dir/number/algebraic_number.c.o
- [ 11%] Building C object src/CMakeFiles/poly.dir/number/dyadic_rational.c.o
- [ 12%] Building C object src/CMakeFiles/static_pic_poly.dir/number/dyadic_rational.c.o
- [ 12%] Building C object src/CMakeFiles/poly.dir/number/algebraic_number.c.o
- [ 13%] Building C object src/CMakeFiles/static_poly.dir/number/value.c.o
- [ 13%] Building C object src/CMakeFiles/poly.dir/number/value.c.o
- [ 13%] Building C object src/CMakeFiles/static_pic_poly.dir/number/algebraic_number.c.o
- [ 13%] Building C object src/CMakeFiles/static_poly.dir/interval/interval.c.o
- [ 14%] Building C object src/CMakeFiles/poly.dir/interval/interval.c.o
- [ 15%] Building C object src/CMakeFiles/static_pic_poly.dir/number/value.c.o
- [ 15%] Building C object src/CMakeFiles/poly.dir/interval/arithmetic.c.o
- [ 16%] Building C object src/CMakeFiles/static_poly.dir/interval/arithmetic.c.o
- [ 16%] Building C object src/CMakeFiles/static_pic_poly.dir/interval/interval.c.o
- [ 16%] Building C object src/CMakeFiles/static_poly.dir/variable/variable_db.c.o
- [ 17%] Building C object src/CMakeFiles/poly.dir/variable/variable_db.c.o
- [ 17%] Building C object src/CMakeFiles/poly.dir/variable/variable_list.c.o
- [ 17%] Building C object src/CMakeFiles/static_pic_poly.dir/interval/arithmetic.c.o
- [ 17%] Building C object src/CMakeFiles/static_poly.dir/variable/variable_list.c.o
- [ 18%] Building C object src/CMakeFiles/static_poly.dir/variable/variable_order.c.o
- [ 19%] Building C object src/CMakeFiles/poly.dir/variable/variable_order.c.o
- [ 19%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/umonomial.c.o
- [ 19%] Building C object src/CMakeFiles/poly.dir/upolynomial/umonomial.c.o
- [ 20%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/upolynomial.c.o
- [ 21%] Building C object src/CMakeFiles/poly.dir/upolynomial/upolynomial.c.o
- [ 22%] Building C object src/CMakeFiles/static_pic_poly.dir/variable/variable_db.c.o
- [ 22%] Building C object src/CMakeFiles/static_pic_poly.dir/variable/variable_list.c.o
- [ 23%] Building C object src/CMakeFiles/static_pic_poly.dir/variable/variable_order.c.o
- [ 23%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/umonomial.c.o
- [ 23%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/output.c.o
- [ 23%] Building C object src/CMakeFiles/poly.dir/upolynomial/output.c.o
- [ 24%] Building C object src/CMakeFiles/poly.dir/upolynomial/upolynomial_dense.c.o
- [ 25%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/upolynomial.c.o
- [ 26%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/upolynomial_dense.c.o
- [ 26%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/output.c.o
- [ 26%] Building C object src/CMakeFiles/poly.dir/upolynomial/bounds.c.o
- [ 26%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/bounds.c.o
- [ 26%] Building C object src/CMakeFiles/poly.dir/upolynomial/gcd.c.o
- [ 27%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/upolynomial_dense.c.o
- [ 28%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/gcd.c.o
- [ 28%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/bounds.c.o
- [ 29%] Building C object src/CMakeFiles/poly.dir/upolynomial/factors.c.o
- [ 29%] Building C object src/CMakeFiles/poly.dir/upolynomial/factorization.c.o
- [ 29%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/gcd.c.o
- [ 29%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/factors.c.o
- [ 30%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/factorization.c.o
- [ 30%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/root_finding.c.o
- [ 31%] Building C object src/CMakeFiles/poly.dir/upolynomial/root_finding.c.o
- [ 32%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/factors.c.o
- [ 32%] Building C object src/CMakeFiles/poly.dir/upolynomial/upolynomial_vector.c.o
- [ 33%] Building C object src/CMakeFiles/poly.dir/polynomial/monomial.c.o
- [ 33%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/factorization.c.o
- [ 33%] Building C object src/CMakeFiles/poly.dir/polynomial/coefficient.c.o
- [ 34%] Building C object src/CMakeFiles/static_poly.dir/polynomial/monomial.c.o
- [ 34%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/upolynomial_vector.c.o
- [ 35%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/root_finding.c.o
- [ 35%] Building C object src/CMakeFiles/static_poly.dir/polynomial/coefficient.c.o
- [ 36%] Building C object src/CMakeFiles/poly.dir/polynomial/output.c.o
- [ 36%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/upolynomial_vector.c.o
- [ 37%] Building C object src/CMakeFiles/static_poly.dir/polynomial/output.c.o
- [ 37%] Building C object src/CMakeFiles/poly.dir/polynomial/gcd.c.o
- [ 38%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/monomial.c.o
- [ 39%] Building C object src/CMakeFiles/poly.dir/polynomial/subres.c.o
- [ 39%] Building C object src/CMakeFiles/static_poly.dir/polynomial/gcd.c.o
- [ 39%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/coefficient.c.o
- [ 39%] Building C object src/CMakeFiles/poly.dir/polynomial/factorization.c.o
- [ 40%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/output.c.o
- [ 40%] Building C object src/CMakeFiles/poly.dir/polynomial/polynomial.c.o
- [ 41%] Building C object src/CMakeFiles/poly.dir/polynomial/polynomial_context.c.o
- [ 41%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/gcd.c.o
- [ 42%] Building C object src/CMakeFiles/static_poly.dir/polynomial/subres.c.o
- [ 42%] Building C object src/CMakeFiles/poly.dir/polynomial/feasibility_set.c.o
- [ 42%] Building C object src/CMakeFiles/static_poly.dir/polynomial/factorization.c.o
- [ 43%] Building C object src/CMakeFiles/static_poly.dir/polynomial/polynomial.c.o
- [ 44%] Building C object src/CMakeFiles/poly.dir/polynomial/feasibility_set_int.c.o
- [ 45%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/subres.c.o
- [ 45%] Building C object src/CMakeFiles/poly.dir/polynomial/polynomial_hash_set.c.o
- [ 45%] Building C object src/CMakeFiles/static_poly.dir/polynomial/polynomial_context.c.o
- [ 45%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/factorization.c.o
- [ 46%] Building C object src/CMakeFiles/poly.dir/polynomial/polynomial_heap.c.o
- [ 47%] Building C object src/CMakeFiles/static_poly.dir/polynomial/feasibility_set.c.o
- [ 47%] Building C object src/CMakeFiles/poly.dir/polynomial/polynomial_vector.c.o
- [ 47%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/polynomial.c.o
- [ 48%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/polynomial_context.c.o
- [ 49%] Building C object src/CMakeFiles/poly.dir/poly.c.o
- [ 49%] Building C object src/CMakeFiles/static_poly.dir/polynomial/feasibility_set_int.c.o
- [ 49%] Building C object src/CMakeFiles/static_poly.dir/polynomial/polynomial_hash_set.c.o
- [ 49%] Linking C shared library libpoly.so
- [ 49%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/feasibility_set.c.o
- [ 50%] Building C object src/CMakeFiles/static_poly.dir/polynomial/polynomial_heap.c.o
- [ 51%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/feasibility_set_int.c.o
- [ 51%] Built target poly
- [ 51%] Building C object src/CMakeFiles/static_poly.dir/polynomial/polynomial_vector.c.o
- [ 51%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/algebraic_number.cpp.o
- [ 52%] Building C object src/CMakeFiles/static_poly.dir/poly.c.o
- [ 52%] Linking C static library libpoly.a
- [ 53%] Building C object python/CMakeFiles/polypy.dir/polypyAlgebraicNumber.c.o
- [ 53%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/polynomial_hash_set.c.o
- [ 53%] Built target static_poly
- [ 54%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/assignment.cpp.o
- [ 55%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/polynomial_heap.c.o
- [ 55%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/polynomial_vector.c.o
- [ 56%] Building C object src/CMakeFiles/static_pic_poly.dir/poly.c.o
- [ 56%] Linking C static library libpicpoly.a
- [ 56%] Built target static_pic_poly
- [ 56%] Building C object python/CMakeFiles/polypy.dir/polypyAssignment.c.o
- [ 56%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/context.cpp.o
- [ 56%] Building C object python/CMakeFiles/polypy.dir/polypyInteger.c.o
- [ 57%] Building C object python/CMakeFiles/polypy.dir/polypyPolynomial.c.o
- [ 58%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/dyadic_interval.cpp.o
- [ 59%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/algebraic_number.cpp.o
- [ 59%] Building C object python/CMakeFiles/polypy.dir/polypy.c.o
- [ 60%] Building C object python/CMakeFiles/polypy.dir/polypyUPolynomial.c.o
- [ 60%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/dyadic_rational.cpp.o
- [ 60%] Building C object python/CMakeFiles/polypy.dir/utils.c.o
- [ 61%] Building C object python/CMakeFiles/polypy.dir/polypyVariable.c.o
- [ 61%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/assignment.cpp.o
- [ 61%] Building C object python/CMakeFiles/polypy.dir/polypyVariableOrder.c.o
- [ 62%] Building C object python/CMakeFiles/polypy.dir/polypyValue.c.o
- [ 63%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/algebraic_number.cpp.o
- [ 64%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/context.cpp.o
- [ 64%] Building C object python/CMakeFiles/polypy.dir/polypyInterval.c.o
- [ 65%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/integer_ring.cpp.o
- [ 65%] Building C object python/CMakeFiles/polypy.dir/polypyFeasibilitySet.c.o
- [ 66%] Linking C shared module polypy.so
- [ 66%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/dyadic_interval.cpp.o
- [ 66%] Built target polypy
- [ 66%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/dyadic_rational.cpp.o
- [ 66%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/assignment.cpp.o
- [ 66%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/integer.cpp.o
- [ 67%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/interval_assignment.cpp.o
- [ 68%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/integer_ring.cpp.o
- [ 68%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/context.cpp.o
- [ 69%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/dyadic_interval.cpp.o
- [ 69%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/interval.cpp.o
- [ 69%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/dyadic_rational.cpp.o
- [ 69%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/integer.cpp.o
- [ 69%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/polynomial.cpp.o
- [ 70%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/polynomial_utils.cpp.o
- [ 71%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/integer_ring.cpp.o
- [ 72%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/interval_assignment.cpp.o
- [ 72%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/integer.cpp.o
- [ 72%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/rational.cpp.o
- [ 72%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/interval.cpp.o
- [ 73%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/rational_interval.cpp.o
- [ 74%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/interval_assignment.cpp.o
- [ 75%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/polynomial.cpp.o
- [ 75%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/sign_condition.cpp.o
- [ 75%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/polynomial_utils.cpp.o
- [ 76%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/upolynomial.cpp.o
- [ 76%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/interval.cpp.o
- [ 76%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/utils.cpp.o
- [ 77%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/rational.cpp.o
- [ 78%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/polynomial.cpp.o
- [ 79%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/value.cpp.o
- [ 79%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/rational_interval.cpp.o
- [ 80%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/sign_condition.cpp.o
- [ 80%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/variable.cpp.o
- [ 80%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/polynomial_utils.cpp.o
- [ 80%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/upolynomial.cpp.o
- [ 80%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/utils.cpp.o
- [ 81%] Linking CXX shared library libpolyxx.so
- [ 82%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/rational.cpp.o
- [ 82%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/rational_interval.cpp.o
- [ 83%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/value.cpp.o
- [ 83%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/sign_condition.cpp.o
- [ 84%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/upolynomial.cpp.o
- [ 84%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/utils.cpp.o
- [ 84%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/variable.cpp.o
- [ 85%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/value.cpp.o
- [ 85%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/variable.cpp.o
- [ 86%] Linking CXX static library libpolyxx.a
- [ 87%] Linking CXX static library libpicpolyxx.a
- [ 87%] Built target static_pic_polyxx
- [ 87%] Built target polyxx
- [ 87%] Building CXX object test/polyxx/CMakeFiles/test_assignment.dir/test_assignment.cpp.o
- [ 87%] Building CXX object test/polyxx/CMakeFiles/test_algebraic_number.dir/test_algebraic_number.cpp.o
- [ 88%] Building CXX object test/poly/CMakeFiles/test_feasible_int_set.dir/test_feasible_int_set.cpp.o
- [ 88%] Built target static_polyxx
- [ 88%] Building CXX object test/polyxx/CMakeFiles/test_dyadic_interval.dir/test_dyadic_interval.cpp.o
- [ 89%] Linking CXX executable test_algebraic_number
- [ 90%] Linking CXX executable test_assignment
- [ 90%] Built target test_algebraic_number
- [ 90%] Building CXX object test/polyxx/CMakeFiles/test_dyadic_rational.dir/test_dyadic_rational.cpp.o
- [ 90%] Built target test_assignment
- [ 91%] Building CXX object test/polyxx/CMakeFiles/test_integer.dir/test_integer.cpp.o
- [ 91%] Linking CXX executable test_feasible_int_set
- [ 91%] Built target test_feasible_int_set
- [ 92%] Building CXX object test/polyxx/CMakeFiles/test_interval.dir/test_interval.cpp.o
- [ 93%] Linking CXX executable test_dyadic_interval
- [ 93%] Built target test_dyadic_interval
- [ 94%] Building CXX object test/polyxx/CMakeFiles/test_interval_assignment.dir/test_interval_assignment.cpp.o
- [ 94%] Linking CXX executable test_dyadic_rational
- [ 94%] Built target test_dyadic_rational
- [ 95%] Building CXX object test/polyxx/CMakeFiles/test_polynomial.dir/test_polynomial.cpp.o
- [ 95%] Linking CXX executable test_integer
- [ 95%] Built target test_integer
- [ 95%] Building CXX object test/polyxx/CMakeFiles/test_rational.dir/test_rational.cpp.o
- [ 95%] Linking CXX executable test_interval
- [ 95%] Linking CXX executable test_interval_assignment
- [ 95%] Built target test_interval
- [ 95%] Building CXX object test/polyxx/CMakeFiles/test_rational_interval.dir/test_rational_interval.cpp.o
- [ 95%] Built target test_interval_assignment
- [ 95%] Building CXX object test/polyxx/CMakeFiles/test_upolynomial.dir/test_upolynomial.cpp.o
- [ 95%] Linking CXX executable test_polynomial
- [ 95%] Built target test_polynomial
- [ 95%] Building CXX object test/polyxx/CMakeFiles/test_value.dir/test_value.cpp.o
- [ 96%] Linking CXX executable test_rational_interval
- [ 96%] Built target test_rational_interval
- [ 96%] Building CXX object test/polyxx/CMakeFiles/test_variable.dir/test_variable.cpp.o
- [ 97%] Linking CXX executable test_rational
- [ 97%] Built target test_rational
- [ 98%] Linking CXX executable test_upolynomial
- [ 98%] Built target test_upolynomial
- [ 99%] Linking CXX executable test_variable
- [100%] Linking CXX executable test_value
- [100%] Built target test_variable
- [100%] Built target test_value
- (cd _build/default/vendor/cvc5 && /usr/bin/bash -e -u -o pipefail -c 'CFLAGS=-fPIC CXXFLAGS=-fPIC ./configure.sh --static -DCMAKE_PREFIX_PATH=$(pkg-config --variable=prefix gmp)')
- -- 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
- -- Found Git: /usr/bin/git (found version "2.47.3")
- fatal: not a git repository: /home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-2/_build/default/vendor/cvc5/../../.git/modules/vendor/cvc5
- -- Building Production build
- -- Performing Test HAVE_C_FLAG_O3
- -- Performing Test HAVE_C_FLAG_O3 - Success
- -- Configuring with C flag '-O3'
- -- Performing Test HAVE_CXX_FLAG_O3
- -- Performing Test HAVE_CXX_FLAG_O3 - Success
- -- Configuring with CXX flag '-O3'
- -- Performing Test HAVE_C_FLAG_Wall
- -- Performing Test HAVE_C_FLAG_Wall - Success
- -- Configuring with C flag '-Wall'
- -- Performing Test HAVE_CXX_FLAG_Wall
- -- Performing Test HAVE_CXX_FLAG_Wall - Success
- -- Configuring with CXX flag '-Wall'
- -- Performing Test HAVE_C_FLAG_Wunused_private_field
- -- Performing Test HAVE_C_FLAG_Wunused_private_field - Failed
- -- Performing Test HAVE_CXX_FLAG_Wunused_private_field
- -- Performing Test HAVE_CXX_FLAG_Wunused_private_field - Failed
- -- Performing Test HAVE_C_FLAG_Wdangling_reference
- -- Performing Test HAVE_C_FLAG_Wdangling_reference - Failed
- -- Performing Test HAVE_CXX_FLAG_Wdangling_reference
- -- Performing Test HAVE_CXX_FLAG_Wdangling_reference - Success
- -- Configuring with CXX flag '-Wno-dangling-reference'
- -- Performing Test HAVE_C_FLAG_fexceptions
- -- Performing Test HAVE_C_FLAG_fexceptions - Success
- -- Configuring with C flag '-fexceptions'
- -- Performing Test HAVE_CXX_FLAG_Wsuggest_override
- -- Performing Test HAVE_CXX_FLAG_Wsuggest_override - Success
- -- Configuring with CXX flag '-Wsuggest-override'
- -- Performing Test HAVE_CXX_FLAG_Wnon_virtual_dtor
- -- Performing Test HAVE_CXX_FLAG_Wnon_virtual_dtor - Success
- -- Configuring with CXX flag '-Wnon-virtual-dtor'
- -- Performing Test HAVE_C_FLAG_Wimplicit_fallthrough
- -- Performing Test HAVE_C_FLAG_Wimplicit_fallthrough - Success
- -- Configuring with C flag '-Wimplicit-fallthrough'
- -- Performing Test HAVE_CXX_FLAG_Wimplicit_fallthrough
- -- Performing Test HAVE_CXX_FLAG_Wimplicit_fallthrough - Success
- -- Configuring with CXX flag '-Wimplicit-fallthrough'
- -- Performing Test HAVE_C_FLAG_Wshadow
- -- Performing Test HAVE_C_FLAG_Wshadow - Success
- -- Configuring with C flag '-Wshadow'
- -- Performing Test HAVE_CXX_FLAG_Wshadow
- -- Performing Test HAVE_CXX_FLAG_Wshadow - Success
- -- Configuring with CXX flag '-Wshadow'
- -- Performing Test HAVE_C_FLAG_fno_operator_names
- -- Performing Test HAVE_C_FLAG_fno_operator_names - Failed
- -- Performing Test HAVE_CXX_FLAG_fno_operator_names
- -- Performing Test HAVE_CXX_FLAG_fno_operator_names - Success
- -- Configuring with CXX flag '-fno-operator-names'
- -- Performing Test HAVE_CXX_FLAG_fno_extern_tls_init
- -- Performing Test HAVE_CXX_FLAG_fno_extern_tls_init - Success
- -- Configuring with CXX flag '-fno-extern-tls-init'
- -- Performing Test HAVE_CXX_FLAG_Wclass_memaccess
- -- Performing Test HAVE_CXX_FLAG_Wclass_memaccess - Success
- -- Configuring with CXX flag '-Wno-class-memaccess'
- -- Disabling unit tests since assertions are disabled.
- -- Found Python: /usr/bin/python3 (found version "3.13.5") found components: Interpreter
- -- Found GMP (unknown version): /usr/lib/x86_64-linux-gnu/libgmp.so
- -- Found CaDiCaL 2.1.3
- : /home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-2/_build/default/vendor/cadical/build/libcadical.a
- -- Found Poly 0.2.0: /home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-2/_build/default/vendor/libpoly/build/src/libpicpoly.a, /home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-2/_build/default/vendor/libpoly/build/src/libpicpolyxx.a
- -- Found SymFPU: /home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-2/_build/default/vendor
- -- Performing Test CVC5_NEED_INT64_T_OVERLOADS
- -- Performing Test CVC5_NEED_INT64_T_OVERLOADS - Failed
- -- Performing Test CVC5_NEED_HASH_UINT64_T_OVERLOAD
- -- Performing Test CVC5_NEED_HASH_UINT64_T_OVERLOAD - Failed
- -- Looking for unistd.h
- -- Looking for unistd.h - found
- -- Looking for sys/wait.h
- -- Looking for sys/wait.h - found
- -- Looking for C++ include ext/stdio_filebuf.h
- -- Looking for C++ include ext/stdio_filebuf.h - found
- -- Looking for clock_gettime
- -- Looking for clock_gettime - found
- -- Looking for ffs
- -- Looking for ffs - found
- -- Looking for optreset
- -- Looking for optreset - not found
- -- Looking for sigaltstack
- -- Looking for sigaltstack - found
- -- Looking for strerror_r
- -- Looking for strerror_r - found
- -- Looking for strtok_r
- -- Looking for strtok_r - found
- -- Looking for setitimer
- -- Looking for setitimer - found
- -- Performing Test STRERROR_R_CHAR_P
- -- Performing Test STRERROR_R_CHAR_P - Failed
- -- Performing Test COMPILER_HAS_HIDDEN_VISIBILITY
- -- Performing Test COMPILER_HAS_HIDDEN_VISIBILITY - Success
- -- Performing Test COMPILER_HAS_HIDDEN_INLINE_VISIBILITY
- -- Performing Test COMPILER_HAS_HIDDEN_INLINE_VISIBILITY - Success
- -- Performing Test COMPILER_HAS_DEPRECATED_ATTR
- -- Performing Test COMPILER_HAS_DEPRECATED_ATTR - Success
-
- cvc5 1.3.0
-
- Build profile : production
-
- Assertions : off
- Debug symbols : off
- Debug context mem mgr : off
-
- Muzzle : off
- Statistics : on
- Tracing : off
-
- ASan : off
- UBSan : off
- TSan : off
- Coverage (gcov) : off
- Profiling (gprof) : off
- Unit tests : off
- Valgrind : off
-
- Shared build : off
- Python bindings : off
- Java bindings : off
- Interprocedural opt. : off
-
- CryptoMiniSat : off
- GLPK : off
- Kissat : off
- LibPoly : on (system)
- CoCoALib : off
- MP library : gmp (system)
- Editline : off
-
- Api docs : off
-
-
- CPPLAGS (-D...): NDEBUG CVC5_STATISTICS_ON CVC5_USE_POLY
- CXXFLAGS : -fPIC -O3 -Wall -Wno-dangling-reference -Wsuggest-override -Wnon-virtual-dtor -Wimplicit-fallthrough -Wshadow -fno-operator-names -fno-extern-tls-init -Wno-class-memaccess
- CFLAGS : -fPIC -O3 -Wall -fexceptions -Wimplicit-fallthrough -Wshadow
- Linker flags :
-
- Install prefix : /usr/local
-
- cvc5 license: modified BSD
-
- Note that this configuration is NOT built against any GPL'ed libraries, so
- it is covered by the (modified) BSD license. To build against GPL'ed
- libraries which can improve cvc5's performance on arithmetic and bit-vector
- logics, use the 'configure.sh' script to re-configure with '--best --gpl'.
-
- Now change to 'build' and type 'make', followed by 'make check' or 'make install'.
-
- -- Configuring done (15.0s)
- -- Generating done (1.2s)
- -- Build files have been written to: /home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-2/_build/default/vendor/cvc5/build
- /usr/bin/bash: line 1: pkg-config: command not found
- (cd _build/default/vendor/cvc5 && /usr/bin/bash -e -u -o pipefail -c 'make -C build -j $(opam var jobs) cvc5')
- make: Entering directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-2/_build/default/vendor/cvc5/build'
- [ 0%] Generating type_enumerator.cpp
- -- Found Git: /usr/bin/git (found version "2.47.3")
- [ 0%] Building CXX object src/context/CMakeFiles/cvc5context.dir/context.cpp.o
- [ 0%] Generating options/options.stamp
- [ 0%] Built target gen-versioninfo
- [ 0%] Building CXX object src/context/CMakeFiles/cvc5context.dir/context_mm.cpp.o
- [ 0%] Built target gen-options
- [ 0%] Generating rewriter_tables.h
- [ 0%] Generating theory_traits.h
- [ 0%] Built target gen-theory
- [ 0%] Generating kind.h
- [ 0%] Generating Trace_tags.h
- [ 0%] Generating metakind.h
- [ 1%] Generating node_manager.h
- [ 1%] Built target gen-tags
- [ 1%] Generating type_checker.cpp
- [ 1%] Generating rewrites.{h,cpp}
- [ 1%] Generating type_properties.h
- [ 1%] Generating kind.cpp
- [ 1%] Building CXX object src/base/CMakeFiles/cvc5base.dir/check.cpp.o
- [ 1%] Built target cvc5context
- [ 1%] Building CXX object src/base/CMakeFiles/cvc5base.dir/configuration.cpp.o
- [ 1%] Generating metakind.cpp
- [ 1%] Generating node_manager.cpp
- [ 1%] Generating type_properties.cpp
- [ 1%] Built target gen-expr
- [ 2%] Building CXX object src/base/CMakeFiles/cvc5base.dir/listener.cpp.o
- [ 2%] Building CXX object src/base/CMakeFiles/cvc5base.dir/exception.cpp.o
- [ 2%] Building CXX object src/base/CMakeFiles/cvc5base.dir/output.cpp.o
- [ 2%] Building CXX object src/base/CMakeFiles/cvc5base.dir/versioninfo.cpp.o
- [ 2%] Built target cvc5base
- [ 2%] Built target gen-rewrites
- [ 2%] Building CXX object src/CMakeFiles/cvc5-obj.dir/api/c/cvc5.cpp.o
- [ 3%] Building CXX object src/CMakeFiles/cvc5-obj.dir/api/c/cvc5_c_structs.cpp.o
- [ 3%] Building CXX object src/CMakeFiles/cvc5-obj.dir/api/cpp/cvc5_types.cpp.o
- [ 3%] Building CXX object src/CMakeFiles/cvc5-obj.dir/api/cpp/cvc5.cpp.o
- [ 3%] Building CXX object src/CMakeFiles/cvc5-obj.dir/api/cpp/cvc5_skolem_id.cpp.o
- [ 3%] Building CXX object src/CMakeFiles/cvc5-obj.dir/decision/assertion_list.cpp.o
- [ 3%] Building CXX object src/CMakeFiles/cvc5-obj.dir/decision/decision_engine.cpp.o
- [ 3%] Building CXX object src/CMakeFiles/cvc5-obj.dir/decision/justification_strategy.cpp.o
- [ 3%] Building CXX object src/CMakeFiles/cvc5-obj.dir/decision/justify_cache.cpp.o
- [ 3%] Building CXX object src/CMakeFiles/cvc5-obj.dir/decision/justify_info.cpp.o
- [ 3%] Building CXX object src/CMakeFiles/cvc5-obj.dir/decision/justify_stack.cpp.o
- [ 5%] Building CXX object src/CMakeFiles/cvc5-obj.dir/decision/justify_stats.cpp.o
- [ 5%] Building C object src/CMakeFiles/cvc5-obj.dir/lib/clock_gettime.c.o
- [ 5%] Building C object src/CMakeFiles/cvc5-obj.dir/lib/ffs.c.o
- [ 5%] Building C object src/CMakeFiles/cvc5-obj.dir/lib/strtok_r.c.o
- [ 5%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/language.cpp.o
- [ 5%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/managed_streams.cpp.o
- [ 5%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/option_exception.cpp.o
- [ 5%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/options_handler.cpp.o
- [ 5%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/assertion_pipeline.cpp.o
- [ 6%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/learned_literal_manager.cpp.o
- [ 6%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/ackermann.cpp.o
- [ 6%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/apply_substs.cpp.o
- [ 6%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/bool_to_bv.cpp.o
- [ 6%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/bv_eager_atoms.cpp.o
- [ 6%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/bv_gauss.cpp.o
- [ 6%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/bv_intro_pow2.cpp.o
- [ 6%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/bv_to_bool.cpp.o
- [ 6%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/bv_to_int.cpp.o
- [ 6%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/extended_rewriter_pass.cpp.o
- [ 7%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/ff_bitsum.cpp.o
- [ 7%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/ff_disjunctive_bit.cpp.o
- [ 7%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/foreign_theory_rewrite.cpp.o
- [ 7%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/fun_def_fmf.cpp.o
- [ 7%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/global_negate.cpp.o
- [ 7%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/ho_elim.cpp.o
- [ 7%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/int_to_bv.cpp.o
- [ 7%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/ite_removal.cpp.o
- [ 7%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/ite_simp.cpp.o
- [ 7%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/learned_rewrite.cpp.o
- [ 8%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/miplib_trick.cpp.o
- [ 8%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/nl_ext_purify.cpp.o
- [ 8%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/non_clausal_simp.cpp.o
- [ 8%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/pseudo_boolean_processor.cpp.o
- [ 8%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/quantifiers_preprocess.cpp.o
- [ 8%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/real_to_int.cpp.o
- [ 8%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/rewrite.cpp.o
- [ 8%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/sep_skolem_emp.cpp.o
- [ 8%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/sort_infer.cpp.o
- [ 8%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/static_learning.cpp.o
- [ 10%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/static_rewrite.cpp.o
- [ 10%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/strings_eager_pp.cpp.o
- [ 10%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/sygus_inference.cpp.o
- [ 10%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/synth_rew_rules.cpp.o
- [ 10%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/theory_preprocess.cpp.o
- [ 10%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/unconstrained_simplifier.cpp.o
- [ 10%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/preprocessing_pass.cpp.o
- [ 10%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/preprocessing_pass_context.cpp.o
- [ 10%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/preprocessing_pass_registry.cpp.o
- [ 11%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/util/boolean_simplification.cpp.o
- [ 11%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/util/ite_utilities.cpp.o
- [ 11%] Building CXX object src/CMakeFiles/cvc5-obj.dir/printer/ast/ast_printer.cpp.o
- [ 11%] Building CXX object src/CMakeFiles/cvc5-obj.dir/printer/enum_to_string.cpp.o
- [ 11%] Building CXX object src/CMakeFiles/cvc5-obj.dir/printer/let_binding.cpp.o
- [ 11%] Building CXX object src/CMakeFiles/cvc5-obj.dir/printer/printer.cpp.o
- [ 11%] Building CXX object src/CMakeFiles/cvc5-obj.dir/printer/smt2/smt2_printer.cpp.o
- [ 11%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/alf/alf_dependent_type_converter.cpp.o
- [ 11%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/alf/alf_list_node_converter.cpp.o
- [ 11%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/alf/alf_node_converter.cpp.o
- [ 12%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/alf/alf_print_channel.cpp.o
- [ 12%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/alf/alf_printer.cpp.o
- [ 12%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/assumption_proof_generator.cpp.o
- [ 12%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/buffered_proof_generator.cpp.o
- [ 12%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/conv_proof_generator.cpp.o
- [ 12%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/conv_seq_proof_generator.cpp.o
- [ 12%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/dot/dot_printer.cpp.o
- [ 12%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/eager_proof_generator.cpp.o
- [ 12%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/lazy_proof.cpp.o
- [ 12%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/lazy_proof_chain.cpp.o
- [ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/lazy_tree_proof_generator.cpp.o
- [ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/lfsc/lfsc_list_sc_node_converter.cpp.o
- [ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/lfsc/lfsc_node_converter.cpp.o
- [ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/lfsc/lfsc_post_processor.cpp.o
- [ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/lfsc/lfsc_printer.cpp.o
- [ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/lfsc/lfsc_print_channel.cpp.o
- [ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/lfsc/lfsc_util.cpp.o
- [ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/method_id.cpp.o
- [ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/print_expr.cpp.o
- [ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof.cpp.o
- [ 15%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof_checker.cpp.o
- [ 15%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof_ensure_closed.cpp.o
- [ 15%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof_generator.cpp.o
- [ 15%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof_letify.cpp.o
- [ 15%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof_node.cpp.o
- [ 15%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof_node_algorithm.cpp.o
- [ 15%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof_node_converter.cpp.o
- [ 15%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof_node_to_sexpr.cpp.o
- [ 15%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof_node_manager.cpp.o
- [ 16%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof_node_updater.cpp.o
- [ 16%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof_rule_checker.cpp.o
- [ 16%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof_step_buffer.cpp.o
- [ 16%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/resolution_proofs_util.cpp.o
- [ 16%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/rewrite_proof_generator.cpp.o
- [ 16%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/subtype_elim_proof_converter.cpp.o
- [ 16%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/trust_id.cpp.o
- [ 16%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/trust_node.cpp.o
- [ 16%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/trust_proof_generator.cpp.o
- [ 16%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/theory_proof_step_buffer.cpp.o
- [ 17%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/unsat_core.cpp.o
- [ 17%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/valid_witness_proof_generator.cpp.o
- [ 17%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/alethe/alethe_let_binding.cpp.o
- [ 17%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/alethe/alethe_node_converter.cpp.o
- [ 17%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/alethe/alethe_post_processor.cpp.o
- [ 17%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/alethe/alethe_printer.cpp.o
- [ 17%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/alethe/alethe_proof_rule.cpp.o
- [ 17%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/cadical.cpp.o
- [ 17%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/cnf_stream.cpp.o
- [ 17%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/cryptominisat.cpp.o
- [ 18%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/kissat.cpp.o
- [ 18%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/learned_db.cpp.o
- [ 18%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/lemma_inprocess.cpp.o
- [ 18%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/minisat/core/Solver.cc.o
- [ 18%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/minisat/minisat.cpp.o
- [ 18%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/minisat/opt_clauses_manager.cpp.o
- [ 18%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/minisat/sat_proof_manager.cpp.o
- [ 18%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/minisat/simp/SimpSolver.cc.o
- [ 18%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/proof_cnf_stream.cpp.o
- [ 18%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/proof_post_processor.cpp.o
- [ 20%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/prop_engine.cpp.o
- [ 20%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/prop_proof_manager.cpp.o
- [ 20%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/sat_solver_factory.cpp.o
- [ 20%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/sat_solver_types.cpp.o
- [ 20%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/skolem_def_manager.cpp.o
- [ 20%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/theory_preregistrar.cpp.o
- [ 20%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/theory_proxy.cpp.o
- [ 20%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/zero_level_learner.cpp.o
- [ 20%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/abduction_solver.cpp.o
- [ 21%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/assertions.cpp.o
- [ 21%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/check_models.cpp.o
- [ 21%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/context_manager.cpp.o
- [ 21%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/difficulty_post_processor.cpp.o
- [ 21%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/env.cpp.o
- [ 21%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/env_obj.cpp.o
- [ 21%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/expand_definitions.cpp.o
- [ 21%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/find_synth_solver.cpp.o
- [ 21%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/listeners.cpp.o
- [ 21%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/illegal_checker.cpp.o
- [ 22%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/interpolation_solver.cpp.o
- [ 22%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/model.cpp.o
- [ 22%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/model_core_builder.cpp.o
- [ 22%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/model_blocker.cpp.o
- [ 22%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/quant_elim_solver.cpp.o
- [ 22%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/preprocessor.cpp.o
- [ 22%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/preprocess_proof_generator.cpp.o
- [ 22%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/print_benchmark.cpp.o
- [ 22%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/process_assertions.cpp.o
- [ 22%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/proof_manager.cpp.o
- [ 23%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/proof_final_callback.cpp.o
- [ 23%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/proof_logger.cpp.o
- [ 23%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/proof_post_processor.cpp.o
- [ 23%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/proof_post_processor_dsl.cpp.o
- [ 23%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/set_defaults.cpp.o
- [ 23%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/solver_engine.cpp.o
- [ 23%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/solver_engine_state.cpp.o
- [ 23%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/solver_engine_stats.cpp.o
- [ 23%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/smt_driver.cpp.o
- [ 23%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/smt_driver_deep_restarts.cpp.o
- [ 25%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/smt_mode.cpp.o
- [ 25%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/smt_solver.cpp.o
- [ 25%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/sygus_solver.cpp.o
- [ 25%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/term_formula_removal.cpp.o
- [ 25%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/timeout_core_manager.cpp.o
- [ 25%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/unsat_core_manager.cpp.o
- [ 25%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/witness_form.cpp.o
- [ 25%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/arith_evaluator.cpp.o
- [ 25%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/arith_ite_utils.cpp.o
- [ 26%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/arith_msum.cpp.o
- [ 26%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/arith_poly_norm.cpp.o
- [ 26%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/arith_preprocess.cpp.o
- [ 26%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/arith_proof_rcons.cpp.o
- [ 26%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/arith_proof_utilities.cpp.o
- [ 26%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/arith_rewriter.cpp.o
- [ 26%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/arith_subs.cpp.o
- [ 26%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/arith_utilities.cpp.o
- [ 26%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/bound_inference.cpp.o
- [ 26%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/branch_and_bound.cpp.o
- [ 27%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/delta_rational.cpp.o
- [ 27%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/equality_solver.cpp.o
- [ 27%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/inference_manager.cpp.o
- [ 27%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/approx_simplex.cpp.o
- [ 27%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/arith_static_learner.cpp.o
- [ 27%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/arithvar.cpp.o
- [ 27%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/attempt_solution_simplex.cpp.o
- [ 27%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/callbacks.cpp.o
- [ 27%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/congruence_manager.cpp.o
- [ 27%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/constraint.cpp.o
- [ 27%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/dio_solver.cpp.o
- [ 28%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/cut_log.cpp.o
- [ 28%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/dual_simplex.cpp.o
- [ 28%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/error_set.cpp.o
- [ 28%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/fc_simplex.cpp.o
- [ 28%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/infer_bounds.cpp.o
- [ 28%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/linear_solver.cpp.o
- [ 28%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/linear_equality.cpp.o
- [ 28%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/matrix.cpp.o
- [ 28%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/normal_form.cpp.o
- [ 30%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/partial_model.cpp.o
- [ 30%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/simplex.cpp.o
- [ 30%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/simplex_update.cpp.o
- [ 30%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/soi_simplex.cpp.o
- [ 30%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/tableau.cpp.o
- [ 30%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/tableau_sizes.cpp.o
- [ 30%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/theory_arith_private.cpp.o
- [ 30%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/coverings_solver.cpp.o
- [ 30%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/coverings/cdcac.cpp.o
- [ 31%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/coverings/cdcac_utils.cpp.o
- [ 31%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/coverings/cocoa_converter.cpp.o
- [ 31%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/coverings/constraints.cpp.o
- [ 31%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/coverings/lazard_evaluation.cpp.o
- [ 31%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/coverings/projections.cpp.o
- [ 31%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/coverings/proof_checker.cpp.o
- [ 31%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/coverings/proof_generator.cpp.o
- [ 31%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/coverings/variable_ordering.cpp.o
- [ 31%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/equality_substitution.cpp.o
- [ 31%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/ext/arith_nl_compare_proof_gen.cpp.o
- [ 32%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/ext/constraint.cpp.o
- [ 32%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/ext/factoring_check.cpp.o
- [ 32%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/ext/monomial.cpp.o
- [ 32%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/ext/monomial_bounds_check.cpp.o
- [ 32%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/ext/monomial_check.cpp.o
- [ 32%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/ext/ext_state.cpp.o
- [ 32%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/ext/proof_checker.cpp.o
- [ 32%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/ext/split_zero_check.cpp.o
- [ 32%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/ext/tangent_plane_check.cpp.o
- [ 32%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/ext_theory_callback.cpp.o
- [ 32%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/icp/candidate.cpp.o
- [ 33%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/iand_solver.cpp.o
- [ 33%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/icp/contraction_origins.cpp.o
- [ 33%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/icp/icp_solver.cpp.o
- [ 33%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/icp/intersection.cpp.o
- [ 33%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/iand_utils.cpp.o
- [ 33%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/nl_lemma_utils.cpp.o
- [ 33%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/nl_model.cpp.o
- [ 33%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/nonlinear_extension.cpp.o
- [ 33%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/poly_conversion.cpp.o
- [ 35%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/pow2_solver.cpp.o
- [ 35%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/stats.cpp.o
- [ 35%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/strategy.cpp.o
- [ 35%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/transcendental/exponential_solver.cpp.o
- [ 35%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/transcendental/proof_checker.cpp.o
- [ 35%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/transcendental/sine_solver.cpp.o
- [ 35%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/transcendental/taylor_generator.cpp.o
- [ 35%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/transcendental/transcendental_solver.cpp.o
- [ 35%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/transcendental/transcendental_state.cpp.o
- [ 35%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/operator_elim.cpp.o
- [ 36%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/pp_rewrite_eq.cpp.o
- [ 36%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/proof_checker.cpp.o
- [ 36%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/rewriter/addition.cpp.o
- [ 36%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/rewriter/node_utils.cpp.o
- [ 36%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/rewriter/rewrite_atom.cpp.o
- [ 36%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/rewrites.cpp.o
- [ 36%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/theory_arith.cpp.o
- [ 36%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/theory_arith_type_rules.cpp.o
- [ 36%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arrays/array_info.cpp.o
- [ 37%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arrays/inference_manager.cpp.o
- [ 37%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arrays/proof_checker.cpp.o
- [ 37%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arrays/skolem_cache.cpp.o
- [ 37%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arrays/theory_arrays.cpp.o
- [ 37%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arrays/theory_arrays_rewriter.cpp.o
- [ 37%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arrays/theory_arrays_type_rules.cpp.o
- [ 37%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arrays/type_enumerator.cpp.o
- [ 37%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/assertion.cpp.o
- [ 37%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/atom_requests.cpp.o
- [ 37%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/bags/bags_rewriter.cpp.o
- [ 38%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/bags/bag_solver.cpp.o
- [ 38%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/bags/bag_reduction.cpp.o
- [ 38%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/bags/bags_statistics.cpp.o
- [ 38%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/bags/bags_utils.cpp.o
- [ 38%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/bags/infer_info.cpp.o
- [ 38%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/bags/inference_generator.cpp.o
- [ 38%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/bags/inference_manager.cpp.o
- [ 38%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/bags/rewrites.cpp.o
- [ 38%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/bags/solver_state.cpp.o
- [ 38%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/bags/strategy.cpp.o
- [ 40%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/bags/term_registry.cpp.o
- [ 40%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/bags/theory_bags.cpp.o
- [ 40%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/bags/theory_bags_type_enumerator.cpp.o
- [ 40%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/bags/theory_bags_type_rules.cpp.o
- [ 40%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/booleans/circuit_propagator.cpp.o
- [ 40%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/booleans/proof_circuit_propagator.cpp.o
- [ 40%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/booleans/proof_checker.cpp.o
- [ 40%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/booleans/theory_bool.cpp.o
- [ 40%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/booleans/theory_bool_rewriter.cpp.o
- [ 40%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/booleans/theory_bool_type_rules.cpp.o
- [ 41%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/builtin/abstract_type.cpp.o
- [ 41%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/builtin/generic_op.cpp.o
- [ 41%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/builtin/proof_checker.cpp.o
- [ 41%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/builtin/theory_builtin.cpp.o
- [ 41%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/builtin/theory_builtin_rewriter.cpp.o
- [ 41%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/builtin/theory_builtin_type_rules.cpp.o
- [ 41%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/builtin/type_enumerator.cpp.o
- [ 41%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/bv/bitblast/bitblast_proof_generator.cpp.o
- [ 41%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/bv/bitblast/node_bitblaster.cpp.o
- [ 42%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/bv/bitblast/proof_bitblaster.cpp.o
- [ 42%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/bv/bv_pp_assert.cpp.o
- [ 42%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/bv/bv_solver_bitblast.cpp.o
- [ 42%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/bv/bv_solver_bitblast_internal.cpp.o
- [ 42%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/bv/macro_rewrite_elaborator.cpp.o
- [ 42%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/bv/int_blaster.cpp.o
- [ 42%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/bv/proof_checker.cpp.o
- [ 42%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/bv/theory_bv.cpp.o
- [ 42%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/bv/theory_bv_rewriter.cpp.o
- [ 42%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/bv/theory_bv_type_rules.cpp.o
- [ 43%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/bv/theory_bv_utils.cpp.o
- [ 43%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/care_pair_argument_callback.cpp.o
- [ 43%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/combination_care_graph.cpp.o
- [ 43%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/combination_engine.cpp.o
- [ 43%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/conflict_processor.cpp.o
- [ 43%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/datatypes/datatypes_rewriter.cpp.o
- [ 43%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/datatypes/inference.cpp.o
- [ 43%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/datatypes/inference_manager.cpp.o
- [ 43%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/datatypes/infer_proof_cons.cpp.o
- [ 43%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/datatypes/proof_checker.cpp.o
- [ 45%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/datatypes/sygus_datatype_utils.cpp.o
- [ 45%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/datatypes/sygus_extension.cpp.o
- [ 45%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/datatypes/sygus_simple_sym.cpp.o
- [ 45%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/datatypes/theory_datatypes.cpp.o
- [ 45%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/datatypes/theory_datatypes_type_rules.cpp.o
- [ 45%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/datatypes/theory_datatypes_utils.cpp.o
- [ 45%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/datatypes/project_op.cpp.o
- [ 45%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/datatypes/tuple_utils.cpp.o
- [ 45%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/datatypes/type_enumerator.cpp.o
- [ 45%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/decision_manager.cpp.o
- [ 46%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/decision_strategy.cpp.o
- [ 46%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/difficulty_manager.cpp.o
- [ 46%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/ee_manager.cpp.o
- [ 46%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/ee_manager_central.cpp.o
- [ 46%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/ee_manager_distributed.cpp.o
- [ 46%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/evaluator.cpp.o
- [ 46%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/ext_theory.cpp.o
- [ 46%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/ff/cocoa_encoder.cpp.o
- [ 46%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/ff/cocoa_util.cpp.o
- [ 47%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/ff/core.cpp.o
- [ 47%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/ff/multi_roots.cpp.o
- [ 47%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/ff/parse.cpp.o
- [ 47%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/ff/split_gb.cpp.o
- [ 47%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/ff/stats.cpp.o
- [ 47%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/ff/sub_theory.cpp.o
- [ 47%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/ff/theory_ff.cpp.o
- [ 47%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/ff/theory_ff_rewriter.cpp.o
- [ 47%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/ff/theory_ff_type_rules.cpp.o
- [ 47%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/ff/uni_roots.cpp.o
- [ 48%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/ff/util.cpp.o
- [ 48%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/fp/fp_word_blaster.cpp.o
- [ 48%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/fp/fp_expand_defs.cpp.o
- [ 48%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/fp/theory_fp.cpp.o
- [ 48%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/fp/theory_fp_rewriter.cpp.o
- [ 48%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/fp/theory_fp_type_rules.cpp.o
- [ 48%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/fp/theory_fp_utils.cpp.o
- [ 48%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/incomplete_id.cpp.o
- [ 48%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/inference_id.cpp.o
- [ 48%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/inference_manager_buffered.cpp.o
- [ 50%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/lemma_property.cpp.o
- [ 50%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/logic_info.cpp.o
- [ 50%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/model_manager.cpp.o
- [ 50%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/model_manager_distributed.cpp.o
- [ 50%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/output_channel.cpp.o
- [ 50%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/alpha_equivalence.cpp.o
- [ 50%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/bv_inverter.cpp.o
- [ 50%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/bv_inverter_utils.cpp.o
- [ 50%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/candidate_rewrite_database.cpp.o
- [ 50%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/candidate_rewrite_filter.cpp.o
- [ 51%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp.o
- [ 51%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp.o
- [ 51%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp.o
- [ 51%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp.o
- [ 51%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/cegqi/ceg_instantiator.cpp.o
- [ 51%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/cegqi/ceg_utils.cpp.o
- [ 51%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp.o
- [ 51%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/cegqi/instantiator.cpp.o
- [ 51%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/cegqi/nested_qe.cpp.o
- [ 52%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/cegqi/vts_term_cache.cpp.o
- [ 52%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/conjecture_generator.cpp.o
- [ 52%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/dynamic_rewrite.cpp.o
- [ 52%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/ematching/candidate_generator.cpp.o
- [ 52%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/ematching/ho_trigger.cpp.o
- [ 52%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/ematching/im_generator.cpp.o
- [ 52%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/ematching/inst_match_generator.cpp.o
- [ 52%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/ematching/inst_match_generator_multi.cpp.o
- [ 52%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp.o
- [ 52%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/ematching/inst_match_generator_simple.cpp.o
- [ 53%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/ematching/inst_strategy.cpp.o
- [ 53%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/ematching/inst_strategy_e_matching.cpp.o
- [ 53%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp.o
- [ 53%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/ematching/instantiation_engine.cpp.o
- [ 53%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/ematching/pattern_term_selector.cpp.o
- [ 53%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/ematching/relational_match_generator.cpp.o
- [ 53%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/ematching/trigger.cpp.o
- [ 53%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/ematching/trigger_database.cpp.o
- [ 53%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/ematching/trigger_term_info.cpp.o
- [ 53%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/ematching/trigger_trie.cpp.o
- [ 55%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/ematching/var_match_generator.cpp.o
- [ 55%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/entailment_check.cpp.o
- [ 55%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/equality_query.cpp.o
- [ 55%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/expr_miner.cpp.o
- [ 55%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/expr_miner_manager.cpp.o
- [ 55%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/extended_rewrite.cpp.o
- [ 55%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/first_order_model.cpp.o
- [ 55%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/fmf/bounded_integers.cpp.o
- [ 55%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/fmf/first_order_model_fmc.cpp.o
- [ 55%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/fmf/full_model_check.cpp.o
- [ 56%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/fmf/model_builder.cpp.o
- [ 56%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/fmf/model_engine.cpp.o
- [ 56%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/fun_def_evaluator.cpp.o
- [ 56%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/ho_term_database.cpp.o
- [ 56%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/ieval/free_var_info.cpp.o
- [ 56%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/ieval/inst_evaluator.cpp.o
- [ 56%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/ieval/inst_evaluator_manager.cpp.o
- [ 56%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/ieval/pattern_term_info.cpp.o
- [ 56%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/ieval/quant_info.cpp.o
- [ 57%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/ieval/state.cpp.o
- [ 57%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/ieval/term_evaluator.cpp.o
- [ 57%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/index_trie.cpp.o
- [ 57%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/inst_match.cpp.o
- [ 57%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/inst_match_trie.cpp.o
- [ 57%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/inst_strategy_enumerative.cpp.o
- [ 57%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/inst_strategy_mbqi.cpp.o
- [ 57%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/inst_strategy_pool.cpp.o
- [ 57%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/inst_strategy_sub_conflict.cpp.o
- [ 57%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/instantiate.cpp.o
- [ 58%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/instantiation_list.cpp.o
- [ 58%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/lazy_trie.cpp.o
- [ 58%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/master_eq_notify.cpp.o
- [ 58%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/mbqi_enum.cpp.o
- [ 58%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/oracle_checker.cpp.o
- [ 58%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/oracle_engine.cpp.o
- [ 58%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/proof_checker.cpp.o
- [ 58%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/quant_bound_inference.cpp.o
- [ 58%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/quant_conflict_find.cpp.o
- [ 58%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/quant_relevance.cpp.o
- [ 60%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/quant_rep_bound_ext.cpp.o
- [ 60%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/quant_split.cpp.o
- [ 60%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/quant_util.cpp.o
- [ 60%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/quant_module.cpp.o
- [ 60%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/quantifiers_attributes.cpp.o
- [ 60%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/quantifiers_inference_manager.cpp.o
- [ 60%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/quantifiers_macros.cpp.o
- [ 60%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/quantifiers_modules.cpp.o
- [ 60%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/quantifiers_preprocess.cpp.o
- [ 60%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/quantifiers_registry.cpp.o
- [ 61%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/quantifiers_rewriter.cpp.o
- [ 61%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/quantifiers_state.cpp.o
- [ 61%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/quantifiers_statistics.cpp.o
- [ 61%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/query_generator.cpp.o
- [ 61%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/query_generator_sample_sat.cpp.o
- [ 61%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/query_generator_unsat.cpp.o
- [ 61%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/relevant_domain.cpp.o
- [ 61%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/rewrite_verifier.cpp.o
- [ 61%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/single_inv_partition.cpp.o
- [ 62%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/skolemize.cpp.o
- [ 62%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/solution_filter.cpp.o
- [ 62%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/term_pools.cpp.o
- [ 62%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/term_tuple_enumerator.cpp.o
- [ 62%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/ce_guided_single_inv.cpp.o
- [ 62%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/cegis.cpp.o
- [ 62%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/cegis_core_connective.cpp.o
- [ 62%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/cegis_unif.cpp.o
- [ 62%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/example_eval_cache.cpp.o
- [ 62%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/example_infer.cpp.o
- [ 63%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/example_min_eval.cpp.o
- [ 63%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/embedding_converter.cpp.o
- [ 63%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/enum_stream_substitution.cpp.o
- [ 63%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/enum_value_manager.cpp.o
- [ 63%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/print_sygus_to_builtin.cpp.o
- [ 63%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/rcons_obligation.cpp.o
- [ 63%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/rcons_type_info.cpp.o
- [ 63%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/sygus_abduct.cpp.o
- [ 63%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/sygus_enumerator.cpp.o
- [ 63%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/sygus_enumerator_callback.cpp.o
- [ 65%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/sygus_eval_unfold.cpp.o
- [ 65%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/sygus_explain.cpp.o
- [ 65%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/sygus_grammar_cons.cpp.o
- [ 65%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/sygus_grammar_norm.cpp.o
- [ 65%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/sygus_grammar_red.cpp.o
- [ 65%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/sygus_interpol.cpp.o
- [ 65%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/sygus_invariance.cpp.o
- [ 65%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/sygus_module.cpp.o
- [ 65%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/sygus_pbe.cpp.o
- [ 65%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/sygus_process_conj.cpp.o
- [ 66%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/sygus_qe_preproc.cpp.o
- [ 66%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/sygus_random_enumerator.cpp.o
- [ 66%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/sygus_reconstruct.cpp.o
- [ 66%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/sygus_repair_const.cpp.o
- [ 66%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/sygus_stats.cpp.o
- [ 66%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/sygus_unif.cpp.o
- [ 66%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/sygus_unif_io.cpp.o
- [ 66%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/sygus_unif_rl.cpp.o
- [ 66%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/sygus_unif_strat.cpp.o
- [ 66%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/sygus_utils.cpp.o
- [ 67%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/synth_conjecture.cpp.o
- [ 67%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/synth_engine.cpp.o
- [ 67%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/synth_finder.cpp.o
- [ 67%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/synth_verify.cpp.o
- [ 67%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/template_infer.cpp.o
- [ 67%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/term_database_sygus.cpp.o
- [ 67%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/type_info.cpp.o
- [ 67%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/type_node_id_trie.cpp.o
- [ 67%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus/transition_inference.cpp.o
- [ 68%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus_inst.cpp.o
- [ 68%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/sygus_sampler.cpp.o
- [ 68%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/term_database.cpp.o
- [ 68%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/term_enumeration.cpp.o
- [ 68%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/term_registry.cpp.o
- [ 68%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/term_util.cpp.o
- [ 68%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/theory_quantifiers.cpp.o
- [ 68%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers/theory_quantifiers_type_rules.cpp.o
- [ 68%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/quantifiers_engine.cpp.o
- [ 68%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/relevance_manager.cpp.o
- [ 70%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/rep_set.cpp.o
- [ 70%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/rep_set_iterator.cpp.o
- [ 70%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/rewriter.cpp.o
- [ 70%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/sep/theory_sep.cpp.o
- [ 70%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/sep/theory_sep_rewriter.cpp.o
- [ 70%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/sep/theory_sep_type_rules.cpp.o
- [ 70%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/sets/cardinality_extension.cpp.o
- [ 70%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/sets/infer_proof_cons.cpp.o
- [ 70%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/sets/inference_manager.cpp.o
- [ 70%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/sets/proof_checker.cpp.o
- [ 71%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/sets/rels_utils.cpp.o
- [ 71%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/sets/set_reduction.cpp.o
- [ 71%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/sets/skolem_cache.cpp.o
- [ 71%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/sets/solver_state.cpp.o
- [ 71%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/sets/term_registry.cpp.o
- [ 71%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/sets/theory_sets.cpp.o
- [ 71%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/sets/theory_sets_private.cpp.o
- [ 71%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/sets/theory_sets_rels.cpp.o
- [ 71%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/sets/theory_sets_rewriter.cpp.o
- [ 71%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/sets/theory_sets_type_enumerator.cpp.o
- [ 72%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/sets/theory_sets_type_rules.cpp.o
- [ 72%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/shared_solver.cpp.o
- [ 72%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/shared_solver_distributed.cpp.o
- [ 72%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/shared_terms_database.cpp.o
- [ 72%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/skolem_lemma.cpp.o
- [ 72%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/smt_engine_subsolver.cpp.o
- [ 72%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/sort_inference.cpp.o
- [ 72%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/partition_generator.cpp.o
- [ 72%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/plugin_module.cpp.o
- [ 73%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/strings/array_solver.cpp.o
- [ 73%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/strings/array_core_solver.cpp.o
- [ 73%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/strings/arith_entail.cpp.o
- [ 73%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/strings/base_solver.cpp.o
- [ 73%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/strings/code_point_solver.cpp.o
- [ 73%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/strings/core_solver.cpp.o
- [ 73%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/strings/eager_solver.cpp.o
- [ 73%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/strings/extf_solver.cpp.o
- [ 73%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/strings/eqc_info.cpp.o
- [ 73%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/strings/infer_info.cpp.o
- [ 75%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/strings/infer_proof_cons.cpp.o
- [ 75%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/strings/inference_manager.cpp.o
- [ 75%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/strings/model_cons_default.cpp.o
- [ 75%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/strings/normal_form.cpp.o
- [ 75%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/strings/proof_checker.cpp.o
- [ 75%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/strings/regexp_enumerator.cpp.o
- [ 75%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/strings/regexp_elim.cpp.o
- [ 75%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/strings/regexp_entail.cpp.o
- [ 75%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/strings/regexp_eval.cpp.o
- [ 75%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/strings/regexp_operation.cpp.o
- [ 76%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/strings/regexp_solver.cpp.o
- [ 76%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/strings/rewrites.cpp.o
- [ 76%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/strings/sequences_rewriter.cpp.o
- [ 76%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/strings/sequences_stats.cpp.o
- [ 76%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/strings/skolem_cache.cpp.o
- [ 76%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/strings/solver_state.cpp.o
- [ 76%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/strings/strategy.cpp.o
- [ 76%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/strings/strings_entail.cpp.o
- [ 76%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/strings/strings_fmf.cpp.o
- [ 76%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/strings/strings_rewriter.cpp.o
- [ 77%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/strings/theory_strings.cpp.o
- [ 77%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/strings/theory_strings_preprocess.cpp.o
- [ 77%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/strings/theory_strings_type_rules.cpp.o
- [ 77%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/strings/theory_strings_utils.cpp.o
- [ 77%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/strings/term_registry.cpp.o
- [ 77%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/strings/type_enumerator.cpp.o
- [ 77%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/strings/word.cpp.o
- [ 77%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/subs_minimize.cpp.o
- [ 77%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/substitutions.cpp.o
- [ 78%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/term_registration_visitor.cpp.o
- [ 78%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/theory.cpp.o
- [ 78%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/theory_engine.cpp.o
- [ 78%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/theory_engine_module.cpp.o
- [ 78%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/theory_engine_proof_generator.cpp.o
- [ 78%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/theory_id.cpp.o
- [ 78%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/theory_engine_statistics.cpp.o
- [ 78%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/theory_inference.cpp.o
- [ 78%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/theory_inference_manager.cpp.o
- [ 78%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/theory_model.cpp.o
- [ 80%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/theory_model_builder.cpp.o
- [ 80%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/theory_preprocessor.cpp.o
- [ 80%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/theory_rewriter.cpp.o
- [ 80%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/theory_state.cpp.o
- [ 80%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/trust_substitutions.cpp.o
- [ 80%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/type_set.cpp.o
- [ 80%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/uf/cardinality_extension.cpp.o
- [ 80%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/uf/conversions_solver.cpp.o
- [ 80%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/uf/diamonds_proof_generator.cpp.o
- [ 80%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/uf/equality_engine.cpp.o
- [ 81%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/uf/equality_engine_iterator.cpp.o
- [ 81%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/uf/eq_proof.cpp.o
- [ 81%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/uf/function_const.cpp.o
- [ 81%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/uf/lambda_lift.cpp.o
- [ 81%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/uf/proof_checker.cpp.o
- [ 81%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/uf/proof_equality_engine.cpp.o
- [ 81%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/uf/ho_extension.cpp.o
- [ 81%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/uf/symmetry_breaker.cpp.o
- [ 81%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/uf/theory_uf.cpp.o
- [ 81%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/uf/theory_uf_model.cpp.o
- [ 82%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/uf/theory_uf_rewriter.cpp.o
- [ 82%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/uf/theory_uf_type_rules.cpp.o
- [ 82%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/uf/type_enumerator.cpp.o
- [ 82%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/valuation.cpp.o
- [ 82%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/aci_norm.cpp.o
- [ 82%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/annotation_elim_node_converter.cpp.o
- [ 82%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/array_store_all.cpp.o
- [ 82%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/ascription_type.cpp.o
- [ 82%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/attribute.cpp.o
- [ 83%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/bound_var_id.cpp.o
- [ 83%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/bound_var_manager.cpp.o
- [ 83%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/cardinality_constraint.cpp.o
- [ 83%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/codatatype_bound_variable.cpp.o
- [ 83%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/elim_shadow_converter.cpp.o
- [ 83%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/elim_witness_converter.cpp.o
- [ 83%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/emptyset.cpp.o
- [ 83%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/emptybag.cpp.o
- [ 83%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/free_var_cache.cpp.o
- [ 83%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/function_array_const.cpp.o
- [ 85%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/internal_skolem_id.cpp.o
- [ 85%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/match_trie.cpp.o
- [ 85%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/nary_match_trie.cpp.o
- [ 85%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/nary_term_util.cpp.o
- [ 85%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/node.cpp.o
- [ 85%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/node_algorithm.cpp.o
- [ 85%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/node_builder.cpp.o
- [ 85%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/node_converter.cpp.o
- [ 85%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/node_trie.cpp.o
- [ 85%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/node_trie_algorithm.cpp.o
- [ 86%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/node_traversal.cpp.o
- [ 86%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/node_value.cpp.o
- [ 86%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/oracle_caller.cpp.o
- [ 86%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/plugin.cpp.o
- [ 86%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/sequence.cpp.o
- [ 86%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/skolem_manager.cpp.o
- [ 86%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/sort_type_size.cpp.o
- [ 86%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/subtype_elim_node_converter.cpp.o
- [ 86%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/term_canonize.cpp.o
- [ 86%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/term_context.cpp.o
- [ 87%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/term_context_node.cpp.o
- [ 87%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/term_context_stack.cpp.o
- [ 87%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/type_matcher.cpp.o
- [ 87%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/type_node.cpp.o
- [ 87%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/dtype.cpp.o
- [ 87%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/dtype_cons.cpp.o
- [ 87%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/dtype_selector.cpp.o
- [ 87%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/sort_to_term.cpp.o
- [ 87%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/subs.cpp.o
- [ 88%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/sygus_datatype.cpp.o
- [ 88%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/sygus_grammar.cpp.o
- [ 88%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/sygus_term_enumerator.cpp.o
- [ 88%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/variadic_trie.cpp.o
- [ 88%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/non_closed_node_converter.cpp.o
- [ 88%] Building CXX object src/CMakeFiles/cvc5-obj.dir/rewriter/basic_rewrite_rcons.cpp.o
- [ 88%] Building CXX object src/CMakeFiles/cvc5-obj.dir/rewriter/rewrite_db.cpp.o
- [ 88%] Building CXX object src/CMakeFiles/cvc5-obj.dir/rewriter/rewrite_db_proof_cons.cpp.o
- [ 88%] Building CXX object src/CMakeFiles/cvc5-obj.dir/rewriter/rewrite_db_term_process.cpp.o
- [ 88%] Building CXX object src/CMakeFiles/cvc5-obj.dir/rewriter/rewrite_proof_rule.cpp.o
- [ 90%] Building CXX object src/CMakeFiles/cvc5-obj.dir/rewriter/rewrite_proof_status.cpp.o
- [ 90%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/bitvector.cpp.o
- [ 90%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/cocoa_globals.cpp.o
- [ 90%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/cardinality.cpp.o
- [ 90%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/cardinality_class.cpp.o
- [ 90%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/didyoumean.cpp.o
- [ 90%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/divisible.cpp.o
- [ 90%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/finite_field_value.cpp.o
- [ 90%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/floatingpoint.cpp.o
- [ 90%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/floatingpoint_size.cpp.o
- [ 91%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/floatingpoint_literal_symfpu.cpp.o
- [ 91%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/floatingpoint_literal_symfpu_traits.cpp.o
- [ 91%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/index.cpp.o
- [ 91%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/ostream_util.cpp.o
- [ 91%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/poly_util.cpp.o
- [ 91%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/random.cpp.o
- [ 91%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/resource_manager.cpp.o
- [ 91%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/result.cpp.o
- [ 91%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/real_algebraic_number_poly_imp.cpp.o
- [ 91%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/regexp.cpp.o
- [ 92%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/roundingmode.cpp.o
- [ 92%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/safe_print.cpp.o
- [ 92%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/sampler.cpp.o
- [ 92%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/sexpr.cpp.o
- [ 92%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/smt2_quote_string.cpp.o
- [ 92%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/statistics_public.cpp.o
- [ 92%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/statistics_registry.cpp.o
- [ 92%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/statistics_stats.cpp.o
- [ 92%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/statistics_value.cpp.o
- [ 93%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/string.cpp.o
- [ 93%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/synth_result.cpp.o
- [ 93%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/uninterpreted_sort_value.cpp.o
- [ 93%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/utility.cpp.o
- [ 93%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/rational_gmp_imp.cpp.o
- [ 93%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/integer_gmp_imp.cpp.o
- [ 93%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/arith_options.cpp.o
- [ 93%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/arrays_options.cpp.o
- [ 93%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/bags_options.cpp.o
- [ 93%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/base_options.cpp.o
- [ 95%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/booleans_options.cpp.o
- [ 95%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/builtin_options.cpp.o
- [ 95%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/bv_options.cpp.o
- [ 95%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/datatypes_options.cpp.o
- [ 95%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/decision_options.cpp.o
- [ 95%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/expr_options.cpp.o
- [ 95%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/ff_options.cpp.o
- [ 95%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/fp_options.cpp.o
- [ 95%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/main_options.cpp.o
- [ 95%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/parallel_options.cpp.o
- [ 96%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/parser_options.cpp.o
- [ 96%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/printer_options.cpp.o
- [ 96%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/proof_options.cpp.o
- [ 96%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/prop_options.cpp.o
- [ 96%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/quantifiers_options.cpp.o
- [ 96%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/sep_options.cpp.o
- [ 96%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/sets_options.cpp.o
- [ 96%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/smt_options.cpp.o
- [ 96%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/strings_options.cpp.o
- [ 96%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/theory_options.cpp.o
- [ 97%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/uf_options.cpp.o
- [ 97%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/io_utils.cpp.o
- [ 97%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/options.cpp.o
- [ 97%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/options_public.cpp.o
- [ 97%] Building CXX object src/CMakeFiles/cvc5-obj.dir/main/options.cpp.o
- [ 97%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/kind.cpp.o
- [ 97%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/metakind.cpp.o
- [ 97%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/node_manager.cpp.o
- [ 97%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/type_checker.cpp.o
- [ 97%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/type_properties.cpp.o
- [ 98%] Building CXX object src/CMakeFiles/cvc5-obj.dir/rewriter/rewrites.cpp.o
- [ 98%] Building CXX object src/CMakeFiles/cvc5-obj.dir/rewriter/rewrites-arith-rewrites.cpp.o
- [ 98%] Building CXX object src/CMakeFiles/cvc5-obj.dir/rewriter/rewrites-arrays-rewrites.cpp.o
- [ 98%] Building CXX object src/CMakeFiles/cvc5-obj.dir/rewriter/rewrites-booleans-rewrites.cpp.o
- [ 98%] Building CXX object src/CMakeFiles/cvc5-obj.dir/rewriter/rewrites-builtin-rewrites.cpp.o
- [ 98%] Building CXX object src/CMakeFiles/cvc5-obj.dir/rewriter/rewrites-bv-rewrites.cpp.o
- [ 98%] Building CXX object src/CMakeFiles/cvc5-obj.dir/rewriter/rewrites-bv-rewrites-elimination.cpp.o
- [ 98%] Building CXX object src/CMakeFiles/cvc5-obj.dir/rewriter/rewrites-bv-rewrites-simplification.cpp.o
- [ 98%] Building CXX object src/CMakeFiles/cvc5-obj.dir/rewriter/rewrites-sets-rewrites.cpp.o
- [100%] Building CXX object src/CMakeFiles/cvc5-obj.dir/rewriter/rewrites-strings-rewrites.cpp.o
- [100%] Building CXX object src/CMakeFiles/cvc5-obj.dir/rewriter/rewrites-strings-rewrites-regexp-membership.cpp.o
- [100%] Building CXX object src/CMakeFiles/cvc5-obj.dir/rewriter/rewrites-uf-rewrites.cpp.o
- [100%] Building CXX object src/CMakeFiles/cvc5-obj.dir/rewriter/rewrites-arith-rewrites-transcendentals.cpp.o
- [100%] Building CXX object src/CMakeFiles/cvc5-obj.dir/rewriter/rewrites-sets-rewrites-card.cpp.o
- [100%] Building CXX object src/CMakeFiles/cvc5-obj.dir/api/cpp/cvc5_proof_rule.cpp.o
- [100%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/type_enumerator.cpp.o
- [100%] Built target cvc5-obj
- [100%] Linking CXX static library libcvc5.a
- [100%] Built target cvc5
- make: Leaving directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-2/_build/default/vendor/cvc5/build'
- fatal: not a git repository: /home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-2/_build/default/vendor/cvc5/../../.git/modules/vendor/cvc5
-> compiled cvc5.1.3.0-2
-> installed cvc5.1.3.0-2
[WARNING] Opam packages conf-gmp.5, conf-python-3.9.0.0, conf-python-3-dev.1, conf-python3-pyparsing.1 and conf-python3-tomli.1 depend on the following system packages that are no longer installed: libgmp-dev python3 python3-dev python3-pyparsing python3-tomli
- conf-gmp.5: depends on libgmp-dev
- conf-python-3.9.0.0: depends on python3
- conf-python-3-dev.1: depends on python3-dev
- conf-python3-pyparsing.1: depends on python3-pyparsing
- conf-python3-tomli.1: depends on python3-tomli
=== STDERR ===
2026-07-26 11:11.13: OK: build cvc5.1.3.0-2 (runc: 1114.9s, disk: 115KB)
2026-07-26 11:11.13: Job succeeded