← Back to PR #28419
Build Log: cvc5.1.3.0-1
Status: FAILURE
Log Output
Processing: [default: loading data]
[cvc5.1.3.0-1: http]
[cvc5.1.3.0-1: extract]
-> retrieved cvc5.1.3.0-1 (https://github.com/formalsec/ocaml-cvc5/releases/download/v1.3.0-1/ocaml-cvc5-v1.3.0-1.tar.gz)
[cvc5: dune build]
+ /home/opam/.opam/default/bin/dune "build" "-p" "cvc5" "-j" "255" "@install" (CWD=/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1)
- (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-1/_build/default/vendor/cadical/build'
- configure: root directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cadical'
- configure: source directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_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-1/_build/default/vendor/cadical/build/makefile'
- configure: linking '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_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-1/_build/default/vendor/cadical/build"
- make[1]: Entering directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_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-1/_build/default/vendor/cadical/build'
- [WARNING] OPAMCONFIRMLEVEL was ignored because CLI 2.0 was requested and it was introduced in 2.1.
- 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_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.2s)
- -- Generating done (0.1s)
- -- Build files have been written to: /home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_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/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/poly.dir/utils/output.c.o
- [ 1%] Building C object src/CMakeFiles/static_pic_poly.dir/utils/assignment.c.o
- [ 2%] Building C object src/CMakeFiles/static_poly.dir/utils/assignment.c.o
- [ 2%] Building C object src/CMakeFiles/static_pic_poly.dir/utils/debug_trace.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/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/number/rational.c.o
- [ 6%] Building C object src/CMakeFiles/static_poly.dir/utils/u_memstream.c.o
- [ 6%] Building C object src/CMakeFiles/static_pic_poly.dir/number/rational.c.o
- [ 7%] Building C object src/CMakeFiles/static_poly.dir/number/integer.c.o
- [ 8%] Building C object src/CMakeFiles/static_pic_poly.dir/utils/u_memstream.c.o
- [ 8%] Building C object src/CMakeFiles/static_pic_poly.dir/utils/output.c.o
- [ 8%] Building C object src/CMakeFiles/static_pic_poly.dir/utils/statistics.c.o
- [ 5%] Building C object src/CMakeFiles/poly.dir/utils/statistics.c.o
- [ 8%] Building C object src/CMakeFiles/static_poly.dir/utils/output.c.o
- [ 9%] Building C object src/CMakeFiles/poly.dir/number/integer.c.o
- [ 10%] Building C object src/CMakeFiles/poly.dir/number/algebraic_number.c.o
- [ 10%] Building C object src/CMakeFiles/static_poly.dir/number/rational.c.o
- [ 10%] Building C object src/CMakeFiles/static_pic_poly.dir/number/integer.c.o
- [ 11%] Building C object src/CMakeFiles/static_pic_poly.dir/number/dyadic_rational.c.o
- [ 11%] Building C object src/CMakeFiles/static_pic_poly.dir/interval/interval.c.o
- [ 11%] Building C object src/CMakeFiles/static_poly.dir/number/algebraic_number.c.o
- [ 12%] Building C object src/CMakeFiles/static_poly.dir/number/dyadic_rational.c.o
- [ 12%] 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
- [ 10%] Building C object src/CMakeFiles/poly.dir/utils/sign_condition.c.o
- [ 13%] Building C object src/CMakeFiles/poly.dir/number/value.c.o
- [ 14%] Building C object src/CMakeFiles/static_pic_poly.dir/variable/variable_db.c.o
- [ 15%] Building C object src/CMakeFiles/poly.dir/variable/variable_order.c.o
- [ 16%] Building C object src/CMakeFiles/static_pic_poly.dir/number/value.c.o
- [ 16%] Building C object src/CMakeFiles/poly.dir/variable/variable_list.c.o
- [ 17%] Building C object src/CMakeFiles/poly.dir/variable/variable_db.c.o
- [ 18%] Building C object src/CMakeFiles/static_poly.dir/number/value.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_db.c.o
- [ 18%] Building C object src/CMakeFiles/static_pic_poly.dir/variable/variable_list.c.o
- [ 19%] Building C object src/CMakeFiles/static_poly.dir/interval/arithmetic.c.o
- [ 12%] Building C object src/CMakeFiles/poly.dir/utils/u_memstream.c.o
- [ 19%] Building C object src/CMakeFiles/static_pic_poly.dir/interval/arithmetic.c.o
- [ 19%] Building C object src/CMakeFiles/poly.dir/interval/interval.c.o
- [ 13%] Building C object src/CMakeFiles/poly.dir/number/dyadic_rational.c.o
- [ 19%] Building C object src/CMakeFiles/poly.dir/interval/arithmetic.c.o
- [ 21%] Building C object src/CMakeFiles/static_pic_poly.dir/variable/variable_order.c.o
- [ 21%] Building C object src/CMakeFiles/static_poly.dir/variable/variable_order.c.o
- [ 22%] Building C object src/CMakeFiles/poly.dir/upolynomial/upolynomial.c.o
- [ 22%] Building C object src/CMakeFiles/poly.dir/upolynomial/umonomial.c.o
- [ 22%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/umonomial.c.o
- [ 23%] Building C object src/CMakeFiles/poly.dir/upolynomial/upolynomial_dense.c.o
- [ 23%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/umonomial.c.o
- [ 24%] Building C object src/CMakeFiles/poly.dir/upolynomial/output.c.o
- [ 24%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/output.c.o
- [ 24%] Building C object src/CMakeFiles/poly.dir/upolynomial/gcd.c.o
- [ 24%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/upolynomial.c.o
- [ 24%] Building C object src/CMakeFiles/poly.dir/upolynomial/bounds.c.o
- [ 24%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/output.c.o
- [ 24%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/bounds.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
- [ 27%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/upolynomial_dense.c.o
- [ 27%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/gcd.c.o
- [ 27%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/factors.c.o
- [ 27%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/bounds.c.o
- [ 28%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/factorization.c.o
- [ 28%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/gcd.c.o
- [ 29%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/factors.c.o
- [ 29%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/upolynomial_vector.c.o
- [ 30%] Building C object src/CMakeFiles/poly.dir/upolynomial/factors.c.o
- [ 30%] Building C object src/CMakeFiles/poly.dir/upolynomial/factorization.c.o
- [ 31%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/factorization.c.o
- [ 31%] Building C object src/CMakeFiles/poly.dir/upolynomial/upolynomial_vector.c.o
- [ 32%] Building C object src/CMakeFiles/poly.dir/upolynomial/root_finding.c.o
- [ 33%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/monomial.c.o
- [ 33%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/upolynomial_vector.c.o
- [ 33%] Building C object src/CMakeFiles/static_poly.dir/polynomial/coefficient.c.o
- [ 33%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/coefficient.c.o
- [ 33%] Building C object src/CMakeFiles/poly.dir/polynomial/coefficient.c.o
- [ 34%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/output.c.o
- [ 35%] Building C object src/CMakeFiles/static_poly.dir/polynomial/monomial.c.o
- [ 36%] Building C object src/CMakeFiles/poly.dir/polynomial/monomial.c.o
- [ 37%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/root_finding.c.o
- [ 37%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/root_finding.c.o
- [ 37%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/gcd.c.o
- [ 38%] Building C object src/CMakeFiles/poly.dir/polynomial/output.c.o
- [ 38%] Building C object src/CMakeFiles/static_poly.dir/polynomial/gcd.c.o
- [ 39%] Building C object src/CMakeFiles/poly.dir/polynomial/gcd.c.o
- [ 39%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/factorization.c.o
- [ 40%] Building C object src/CMakeFiles/static_poly.dir/polynomial/subres.c.o
- [ 41%] Building C object src/CMakeFiles/poly.dir/polynomial/polynomial.c.o
- [ 41%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/polynomial.c.o
- [ 42%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/subres.c.o
- [ 42%] Building C object src/CMakeFiles/poly.dir/polynomial/subres.c.o
- [ 42%] Building C object src/CMakeFiles/static_poly.dir/polynomial/output.c.o
- [ 42%] Building C object src/CMakeFiles/poly.dir/polynomial/factorization.c.o
- [ 42%] Building C object src/CMakeFiles/static_poly.dir/polynomial/polynomial_context.c.o
- [ 42%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/feasibility_set.c.o
- [ 42%] Building C object src/CMakeFiles/static_poly.dir/polynomial/factorization.c.o
- [ 42%] Building C object src/CMakeFiles/poly.dir/polynomial/polynomial_hash_set.c.o
- [ 43%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/feasibility_set_int.c.o
- [ 48%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/polynomial_heap.c.o
- [ 49%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/polynomial_context.c.o
- [ 50%] Building C object src/CMakeFiles/static_poly.dir/polynomial/polynomial_heap.c.o
- [ 52%] Building C object src/CMakeFiles/poly.dir/polynomial/feasibility_set_int.c.o
- [ 52%] Building C object src/CMakeFiles/poly.dir/polynomial/polynomial_vector.c.o
- [ 46%] Building C object src/CMakeFiles/static_poly.dir/polynomial/polynomial.c.o
- [ 52%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/polynomial_hash_set.c.o
- [ 45%] Building C object src/CMakeFiles/static_poly.dir/polynomial/feasibility_set_int.c.o
- [ 52%] Building C object src/CMakeFiles/poly.dir/polynomial/polynomial_heap.c.o
- [ 52%] Building C object src/CMakeFiles/static_poly.dir/polynomial/polynomial_hash_set.c.o
- [ 53%] Building C object src/CMakeFiles/poly.dir/polynomial/polynomial_context.c.o
- [ 53%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/polynomial_vector.c.o
- [ 47%] Building C object src/CMakeFiles/static_poly.dir/polynomial/feasibility_set.c.o
- [ 53%] Building C object src/CMakeFiles/poly.dir/poly.c.o
- [ 53%] Building C object src/CMakeFiles/static_poly.dir/poly.c.o
- [ 53%] Building C object src/CMakeFiles/poly.dir/polynomial/feasibility_set.c.o
- [ 53%] Building C object src/CMakeFiles/static_poly.dir/polynomial/polynomial_vector.c.o
- [ 54%] Building C object src/CMakeFiles/static_pic_poly.dir/poly.c.o
- [ 54%] Linking C static library libpoly.a
- [ 54%] Linking C static library libpicpoly.a
- [ 54%] Linking C shared library libpoly.so
- [ 54%] Built target static_poly
- [ 54%] Built target static_pic_poly
- [ 54%] Built target poly
- [ 55%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/algebraic_number.cpp.o
- [ 56%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/context.cpp.o
- [ 56%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/assignment.cpp.o
- [ 56%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/dyadic_interval.cpp.o
- [ 56%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/integer.cpp.o
- [ 56%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/dyadic_rational.cpp.o
- [ 56%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/interval.cpp.o
- [ 57%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/integer_ring.cpp.o
- [ 58%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/interval_assignment.cpp.o
- [ 59%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/polynomial.cpp.o
- [ 60%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/assignment.cpp.o
- [ 61%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/dyadic_interval.cpp.o
- [ 62%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/integer_ring.cpp.o
- [ 62%] Building C object python/CMakeFiles/polypy.dir/polypy.c.o
- [ 63%] Building C object python/CMakeFiles/polypy.dir/polypyPolynomial.c.o
- [ 64%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/algebraic_number.cpp.o
- [ 65%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/integer_ring.cpp.o
- [ 66%] Building C object python/CMakeFiles/polypy.dir/polypyUPolynomial.c.o
- [ 66%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/dyadic_rational.cpp.o
- [ 67%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/dyadic_rational.cpp.o
- [ 68%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/interval_assignment.cpp.o
- [ 68%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/interval.cpp.o
- [ 68%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/interval.cpp.o
- [ 69%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/assignment.cpp.o
- [ 69%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/polynomial_utils.cpp.o
- [ 69%] Building C object python/CMakeFiles/polypy.dir/polypyVariableOrder.c.o
- [ 69%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/polynomial.cpp.o
- [ 67%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/utils.cpp.o
- [ 70%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/sign_condition.cpp.o
- [ 73%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/dyadic_interval.cpp.o
- [ 73%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/rational.cpp.o
- [ 73%] Building C object python/CMakeFiles/polypy.dir/polypyAlgebraicNumber.c.o
- [ 73%] Building C object python/CMakeFiles/polypy.dir/polypyAssignment.c.o
- [ 73%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/context.cpp.o
- [ 73%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/context.cpp.o
- [ 73%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/rational_interval.cpp.o
- [ 73%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/algebraic_number.cpp.o
- [ 73%] Building C object python/CMakeFiles/polypy.dir/polypyInteger.c.o
- [ 71%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/polynomial.cpp.o
- [ 73%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/sign_condition.cpp.o
- [ 72%] Building C object python/CMakeFiles/polypy.dir/polypyValue.c.o
- [ 73%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/integer.cpp.o
- [ 73%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/integer.cpp.o
- [ 74%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/polynomial_utils.cpp.o
- [ 74%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/sign_condition.cpp.o
- [ 74%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/rational.cpp.o
- [ 75%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/value.cpp.o
- [ 75%] Building C object python/CMakeFiles/polypy.dir/polypyInterval.c.o
- [ 76%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/upolynomial.cpp.o
- [ 77%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/upolynomial.cpp.o
- [ 77%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/utils.cpp.o
- [ 78%] Building C object python/CMakeFiles/polypy.dir/polypyVariable.c.o
- [ 76%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/utils.cpp.o
- [ 78%] Building C object python/CMakeFiles/polypy.dir/utils.c.o
- [ 79%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/rational.cpp.o
- [ 80%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/interval_assignment.cpp.o
- [ 81%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/value.cpp.o
- [ 81%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/polynomial_utils.cpp.o
- [ 81%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/variable.cpp.o
- [ 82%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/value.cpp.o
- [ 81%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/upolynomial.cpp.o
- [ 82%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/variable.cpp.o
- [ 82%] Building C object python/CMakeFiles/polypy.dir/polypyFeasibilitySet.c.o
- [ 82%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/rational_interval.cpp.o
- [ 83%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/rational_interval.cpp.o
- [ 83%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/variable.cpp.o
- [ 84%] Linking C shared module polypy.so
- [ 84%] Built target polypy
- [ 85%] Linking CXX static library libpolyxx.a
- [ 86%] Linking CXX shared library libpolyxx.so
- [ 87%] Linking CXX static library libpicpolyxx.a
- [ 87%] Built target static_polyxx
- [ 87%] Built target static_pic_polyxx
- [ 87%] Built target polyxx
- [ 87%] Building CXX object test/polyxx/CMakeFiles/test_algebraic_number.dir/test_algebraic_number.cpp.o
- [ 90%] Building CXX object test/polyxx/CMakeFiles/test_dyadic_rational.dir/test_dyadic_rational.cpp.o
- [ 91%] Building CXX object test/polyxx/CMakeFiles/test_integer.dir/test_integer.cpp.o
- [ 88%] Building CXX object test/polyxx/CMakeFiles/test_dyadic_interval.dir/test_dyadic_interval.cpp.o
- [ 92%] Building CXX object test/polyxx/CMakeFiles/test_value.dir/test_value.cpp.o
- [ 92%] Building CXX object test/poly/CMakeFiles/test_feasible_int_set.dir/test_feasible_int_set.cpp.o
- [ 92%] Building CXX object test/polyxx/CMakeFiles/test_assignment.dir/test_assignment.cpp.o
- [ 92%] Building CXX object test/polyxx/CMakeFiles/test_rational_interval.dir/test_rational_interval.cpp.o
- [ 92%] Building CXX object test/polyxx/CMakeFiles/test_variable.dir/test_variable.cpp.o
- [ 92%] Building CXX object test/polyxx/CMakeFiles/test_upolynomial.dir/test_upolynomial.cpp.o
- [ 92%] Building CXX object test/polyxx/CMakeFiles/test_interval_assignment.dir/test_interval_assignment.cpp.o
- [ 92%] Building CXX object test/polyxx/CMakeFiles/test_rational.dir/test_rational.cpp.o
- [ 92%] Building CXX object test/polyxx/CMakeFiles/test_interval.dir/test_interval.cpp.o
- [ 92%] Building CXX object test/polyxx/CMakeFiles/test_polynomial.dir/test_polynomial.cpp.o
- [ 93%] Linking CXX executable test_variable
- [ 93%] Linking CXX executable test_interval_assignment
- [ 94%] Linking CXX executable test_assignment
- [ 95%] Linking CXX executable test_algebraic_number
- [ 96%] Linking CXX executable test_rational_interval
- [ 96%] Linking CXX executable test_polynomial
- [ 96%] Built target test_variable
- [ 96%] Built target test_assignment
- [ 96%] Built target test_interval_assignment
- [ 97%] Linking CXX executable test_dyadic_interval
- [ 97%] Built target test_algebraic_number
- [ 97%] Built target test_rational_interval
- [ 97%] Linking CXX executable test_integer
- [ 97%] Built target test_polynomial
- [ 98%] Linking CXX executable test_rational
- [ 98%] Linking CXX executable test_dyadic_rational
- [ 98%] Built target test_dyadic_interval
- [ 98%] Built target test_integer
- [ 98%] Linking CXX executable test_interval
- [ 98%] Built target test_dyadic_rational
- [ 99%] Linking CXX executable test_value
- [ 99%] Linking CXX executable test_feasible_int_set
- [ 99%] Built target test_interval
- [ 99%] Built target test_value
- [ 99%] Built target test_rational
- [100%] Linking CXX executable test_upolynomial
- [100%] Built target test_feasible_int_set
- [100%] Built target test_upolynomial
- [WARNING] OPAMCONFIRMLEVEL was ignored because CLI 2.0 was requested and it was introduced in 2.1.
- (cd _build/default/vendor/cvc5 && /usr/bin/bash -e -u -o pipefail -c './configure.sh --static')
- -- 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-1/_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.a
- -- Found CaDiCaL 2.1.3
- : /home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cadical/build/libcadical.a
- -- Found Poly 0.2.0: /home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/libpoly/build/src/libpicpoly.a, /home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/libpoly/build/src/libpicpolyxx.a
- -- Found SymFPU: /home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_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 : -O3 -Wall -Wno-dangling-reference -Wsuggest-override -Wnon-virtual-dtor -Wimplicit-fallthrough -Wshadow -fno-operator-names -fno-extern-tls-init -Wno-class-memaccess
- CFLAGS : -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 (9.8s)
- -- Generating done (0.7s)
- -- Build files have been written to: /home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build
- File "dune", lines 7-41, characters 0-972:
- 7 | (rule
- 8 | (deps
- 9 | (source_tree vendor))
- ....
- 39 | (bash "make -C build -j $(opam var jobs)")))
- 40 | (copy vendor/cvc5/build/src/libcvc5.a libcvc5.a)
- 41 | (copy vendor/cvc5/build/include/cvc5/cvc5_export.h cvc5_export.h)))))
- (cd _build/default/vendor/cvc5 && /usr/bin/bash -e -u -o pipefail -c 'make -C build -j $(opam var jobs)')
- make: Entering directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build'
- -- Found Git: /usr/bin/git (found version "2.47.3")
- [ 0%] Generating kind.h
- [ 0%] Generating type_enumerator.cpp
- [ 0%] Generating options/options.stamp
- [ 0%] Generating rewriter_tables.h
- [ 0%] Generating theory_traits.h
- [ 0%] Building CXX object src/context/CMakeFiles/cvc5context.dir/context.cpp.o
- [ 0%] Generating type_properties.h
- [ 0%] Generating type_checker.cpp
- [ 1%] Generating node_manager.h
- [ 0%] Generating metakind.h
- [ 1%] Building CXX object src/context/CMakeFiles/cvc5context.dir/context_mm.cpp.o
- [ 2%] Generating smt2_tokens.h
- [ 2%] Generating Trace_tags.h
- [ 2%] Generating rewrites.{h,cpp}
- [ 2%] Built target gen-versioninfo
- [ 2%] Built target gen-tokens
- [ 2%] Generating metakind.cpp
- [ 2%] Generating kind.cpp
- [ 2%] Built target gen-theory
- [ 2%] Generating type_properties.cpp
- [ 2%] Generating node_manager.cpp
- [ 2%] Built target gen-options
- [ 2%] Built target gen-tags
- [ 2%] Built target gen-expr
- [ 2%] Building CXX object src/base/CMakeFiles/cvc5base.dir/check.cpp.o
- [ 2%] Building CXX object src/base/CMakeFiles/cvc5base.dir/configuration.cpp.o
- [ 3%] Building CXX object src/base/CMakeFiles/cvc5base.dir/listener.cpp.o
- [ 3%] Building CXX object src/base/CMakeFiles/cvc5base.dir/output.cpp.o
- [ 2%] Building CXX object src/base/CMakeFiles/cvc5base.dir/exception.cpp.o
- [ 3%] Building CXX object src/base/CMakeFiles/cvc5base.dir/versioninfo.cpp.o
- [ 3%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/commands.cpp.o
- [ 3%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/command_status.cpp.o
- [ 4%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/parser.cpp.o
- [ 4%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/input.cpp.o
- [ 3%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/lexer.cpp.o
- [ 4%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/parser_state.cpp.o
- [ 4%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/parse_op.cpp.o
- [ 4%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/parser_utils.cpp.o
- [ 4%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/smt2/smt2_state.cpp.o
- [ 4%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/smt2/smt2_cmd_parser.cpp.o
- [ 4%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/smt2/smt2_parser.cpp.o
- [ 4%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/smt2/smt2_lexer.cpp.o
- [ 4%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/smt2/smt2_term_parser.cpp.o
- [ 4%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/sym_manager.cpp.o
- [ 5%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/symbol_table.cpp.o
- [ 5%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/tokens.cpp.o
- [ 5%] Built target cvc5context
- [ 5%] Built target cvc5base
- [ 5%] Built target gen-rewrites
- [ 5%] Building CXX object src/CMakeFiles/cvc5-obj.dir/api/c/cvc5.cpp.o
- [ 7%] Building CXX object src/CMakeFiles/cvc5-obj.dir/api/c/cvc5_c_structs.cpp.o
- [ 7%] Building CXX object src/CMakeFiles/cvc5-obj.dir/api/cpp/cvc5_types.cpp.o
- [ 7%] Building CXX object src/CMakeFiles/cvc5-obj.dir/decision/justify_info.cpp.o
- [ 7%] Building CXX object src/CMakeFiles/cvc5-obj.dir/api/cpp/cvc5_skolem_id.cpp.o
- [ 7%] Building CXX object src/CMakeFiles/cvc5-obj.dir/decision/justify_stack.cpp.o
- [ 8%] Building CXX object src/CMakeFiles/cvc5-obj.dir/decision/justify_cache.cpp.o
- [ 8%] Building CXX object src/CMakeFiles/cvc5-obj.dir/decision/justify_stats.cpp.o
- [ 8%] Building C object src/CMakeFiles/cvc5-obj.dir/lib/clock_gettime.c.o
- [ 8%] Building C object src/CMakeFiles/cvc5-obj.dir/lib/ffs.c.o
- [ 8%] Building CXX object src/CMakeFiles/cvc5-obj.dir/decision/assertion_list.cpp.o
- [ 8%] Building C object src/CMakeFiles/cvc5-obj.dir/lib/strtok_r.c.o
- [ 8%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/language.cpp.o
- [ 8%] Building CXX object src/CMakeFiles/cvc5-obj.dir/decision/decision_engine.cpp.o
- [ 8%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/managed_streams.cpp.o
- [ 8%] Building CXX object src/CMakeFiles/cvc5-obj.dir/api/cpp/cvc5.cpp.o
- [ 8%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/option_exception.cpp.o
- [ 8%] Building CXX object src/CMakeFiles/cvc5-obj.dir/decision/justification_strategy.cpp.o
- [ 8%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/options_handler.cpp.o
- [ 8%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/assertion_pipeline.cpp.o
- [ 9%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/learned_literal_manager.cpp.o
- [ 9%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/ackermann.cpp.o
- [ 9%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/apply_substs.cpp.o
- [ 9%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/bool_to_bv.cpp.o
- [ 9%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/bv_eager_atoms.cpp.o
- [ 9%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/bv_gauss.cpp.o
- [ 9%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/bv_intro_pow2.cpp.o
- [ 9%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/bv_to_bool.cpp.o
- [ 9%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/bv_to_int.cpp.o
- [ 9%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/extended_rewriter_pass.cpp.o
- [ 10%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/ff_bitsum.cpp.o
- [ 10%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/ff_disjunctive_bit.cpp.o
- [ 10%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/foreign_theory_rewrite.cpp.o
- [ 10%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/fun_def_fmf.cpp.o
- [ 10%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/global_negate.cpp.o
- [ 10%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/ho_elim.cpp.o
- [ 10%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/int_to_bv.cpp.o
- [ 10%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/ite_simp.cpp.o
- [ 10%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/ite_removal.cpp.o
- [ 10%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/learned_rewrite.cpp.o
- [ 11%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/miplib_trick.cpp.o
- [ 11%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/nl_ext_purify.cpp.o
- [ 11%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/non_clausal_simp.cpp.o
- [ 11%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/pseudo_boolean_processor.cpp.o
- [ 11%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/quantifiers_preprocess.cpp.o
- [ 11%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/real_to_int.cpp.o
- [ 11%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/rewrite.cpp.o
- [ 11%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/sep_skolem_emp.cpp.o
- [ 11%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/sort_infer.cpp.o
- [ 11%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/static_learning.cpp.o
- [ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/static_rewrite.cpp.o
- [ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/strings_eager_pp.cpp.o
- [ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/sygus_inference.cpp.o
- [ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/synth_rew_rules.cpp.o
- [ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/theory_preprocess.cpp.o
- [ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/unconstrained_simplifier.cpp.o
- [ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/preprocessing_pass.cpp.o
- [ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/preprocessing_pass_context.cpp.o
- [ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/preprocessing_pass_registry.cpp.o
- [ 14%] Building CXX object src/CMakeFiles/cvc5-obj.dir/printer/ast/ast_printer.cpp.o
- [ 14%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/util/boolean_simplification.cpp.o
- [ 14%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/util/ite_utilities.cpp.o
- [ 14%] Building CXX object src/CMakeFiles/cvc5-obj.dir/printer/enum_to_string.cpp.o
- [ 14%] Building CXX object src/CMakeFiles/cvc5-obj.dir/printer/let_binding.cpp.o
- [ 14%] Building CXX object src/CMakeFiles/cvc5-obj.dir/printer/printer.cpp.o
- [ 14%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/alf/alf_dependent_type_converter.cpp.o
- [ 14%] Building CXX object src/CMakeFiles/cvc5-obj.dir/printer/smt2/smt2_printer.cpp.o
- [ 14%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/alf/alf_list_node_converter.cpp.o
- [ 14%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/alf/alf_node_converter.cpp.o
- [ 15%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/alf/alf_print_channel.cpp.o
- [ 15%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/alf/alf_printer.cpp.o
- [ 15%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/assumption_proof_generator.cpp.o
- [ 15%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/buffered_proof_generator.cpp.o
- [ 15%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/conv_proof_generator.cpp.o
- [ 15%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/conv_seq_proof_generator.cpp.o
- [ 15%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/dot/dot_printer.cpp.o
- [ 15%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/lazy_proof.cpp.o
- [ 15%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/lazy_proof_chain.cpp.o
- [ 15%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/eager_proof_generator.cpp.o
- [ 16%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/lazy_tree_proof_generator.cpp.o
- [ 16%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/lfsc/lfsc_list_sc_node_converter.cpp.o
- [ 16%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/lfsc/lfsc_post_processor.cpp.o
- [ 16%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/lfsc/lfsc_node_converter.cpp.o
- [ 16%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/lfsc/lfsc_print_channel.cpp.o
- [ 16%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/lfsc/lfsc_printer.cpp.o
- [ 16%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/lfsc/lfsc_util.cpp.o
- [ 16%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/method_id.cpp.o
- [ 16%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/print_expr.cpp.o
- [ 16%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof.cpp.o
- [ 17%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof_checker.cpp.o
- [ 17%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof_ensure_closed.cpp.o
- [ 17%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof_letify.cpp.o
- [ 17%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof_generator.cpp.o
- [ 17%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof_node.cpp.o
- [ 17%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof_node_algorithm.cpp.o
- [ 17%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof_node_to_sexpr.cpp.o
- [ 17%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof_node_manager.cpp.o
- [ 19%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof_node_updater.cpp.o
- [ 19%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof_rule_checker.cpp.o
- [ 19%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof_node_converter.cpp.o
- [ 19%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof_step_buffer.cpp.o
- [ 19%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/resolution_proofs_util.cpp.o
- [ 19%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/rewrite_proof_generator.cpp.o
- [ 19%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/subtype_elim_proof_converter.cpp.o
- [ 19%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/trust_id.cpp.o
- [ 19%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/trust_node.cpp.o
- [ 19%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/trust_proof_generator.cpp.o
- [ 19%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/theory_proof_step_buffer.cpp.o
- [ 20%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/unsat_core.cpp.o
- [ 20%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/valid_witness_proof_generator.cpp.o
- [ 20%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/alethe/alethe_let_binding.cpp.o
- [ 20%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/alethe/alethe_node_converter.cpp.o
- [ 20%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/alethe/alethe_post_processor.cpp.o
- [ 20%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/alethe/alethe_printer.cpp.o
- [ 20%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/alethe/alethe_proof_rule.cpp.o
- [ 20%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/cadical.cpp.o
- [ 20%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/cnf_stream.cpp.o
- [ 20%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/cryptominisat.cpp.o
- [ 20%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/learned_db.cpp.o
- [ 21%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/kissat.cpp.o
- [ 21%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/lemma_inprocess.cpp.o
- [ 21%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/minisat/core/Solver.cc.o
- [ 21%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/minisat/minisat.cpp.o
- [ 21%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/minisat/opt_clauses_manager.cpp.o
- [ 21%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/minisat/sat_proof_manager.cpp.o
- [ 21%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/minisat/simp/SimpSolver.cc.o
- [ 21%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/proof_cnf_stream.cpp.o
- [ 21%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/proof_post_processor.cpp.o
- [ 22%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/prop_engine.cpp.o
- [ 22%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/prop_proof_manager.cpp.o
- [ 22%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/sat_solver_factory.cpp.o
- [ 22%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/sat_solver_types.cpp.o
- [ 22%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/skolem_def_manager.cpp.o
- [ 22%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/zero_level_learner.cpp.o
- [ 23%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/assertions.cpp.o
- [ 23%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/check_models.cpp.o
- [ 23%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/theory_preregistrar.cpp.o
- [ 23%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/context_manager.cpp.o
- [ 23%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/abduction_solver.cpp.o
- [ 23%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/theory_proxy.cpp.o
- [ 23%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/difficulty_post_processor.cpp.o
- [ 23%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/env.cpp.o
- [ 23%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/expand_definitions.cpp.o
- [ 23%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/env_obj.cpp.o
- [ 23%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/find_synth_solver.cpp.o
- [ 23%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/listeners.cpp.o
- [ 23%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/illegal_checker.cpp.o
- [ 25%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/interpolation_solver.cpp.o
- [ 25%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/model_blocker.cpp.o
- [ 25%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/model.cpp.o
- [ 25%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/model_core_builder.cpp.o
- [ 25%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/quant_elim_solver.cpp.o
- [ 25%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/preprocessor.cpp.o
- [ 25%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/print_benchmark.cpp.o
- [ 25%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/preprocess_proof_generator.cpp.o
- [ 25%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/process_assertions.cpp.o
- [ 26%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/proof_final_callback.cpp.o
- [ 26%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/proof_post_processor.cpp.o
- [ 26%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/proof_manager.cpp.o
- [ 26%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/proof_logger.cpp.o
- [ 26%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/proof_post_processor_dsl.cpp.o
- [ 26%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/set_defaults.cpp.o
- [ 26%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/solver_engine.cpp.o
- [ 26%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/solver_engine_state.cpp.o
- [ 26%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/solver_engine_stats.cpp.o
- [ 26%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/smt_driver.cpp.o
- [ 26%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/smt_driver_deep_restarts.cpp.o
- [ 27%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/smt_mode.cpp.o
- [ 27%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/sygus_solver.cpp.o
- [ 27%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/smt_solver.cpp.o
- [ 27%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/term_formula_removal.cpp.o
- [ 27%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/timeout_core_manager.cpp.o
- [ 27%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/unsat_core_manager.cpp.o
- [ 27%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/witness_form.cpp.o
- [ 27%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/arith_evaluator.cpp.o
- [ 27%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/arith_ite_utils.cpp.o
- [ 28%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/arith_msum.cpp.o
- [ 28%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/arith_poly_norm.cpp.o
- [ 28%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/arith_preprocess.cpp.o
- [ 28%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/arith_proof_rcons.cpp.o
- [ 28%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/arith_proof_utilities.cpp.o
- [ 28%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/arith_subs.cpp.o
- [ 28%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/arith_utilities.cpp.o
- [ 28%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/arith_rewriter.cpp.o
- [ 28%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/bound_inference.cpp.o
- [ 28%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/branch_and_bound.cpp.o
- [ 29%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/delta_rational.cpp.o
- [ 29%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/equality_solver.cpp.o
- [ 29%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/inference_manager.cpp.o
- [ 29%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/approx_simplex.cpp.o
- [ 29%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/arith_static_learner.cpp.o
- [ 29%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/arithvar.cpp.o
- [ 29%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/attempt_solution_simplex.cpp.o
- [ 29%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/callbacks.cpp.o
- [ 29%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/congruence_manager.cpp.o
- [ 29%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/constraint.cpp.o
- [ 30%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/cut_log.cpp.o
- [ 30%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/dio_solver.cpp.o
- [ 30%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/dual_simplex.cpp.o
- [ 30%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/error_set.cpp.o
- [ 30%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/fc_simplex.cpp.o
- [ 30%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/infer_bounds.cpp.o
- [ 30%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/linear_solver.cpp.o
- [ 30%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/linear_equality.cpp.o
- [ 30%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/matrix.cpp.o
- [ 30%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/normal_form.cpp.o
- [ 32%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/partial_model.cpp.o
- [ 32%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/simplex.cpp.o
- [ 32%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/simplex_update.cpp.o
- [ 32%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/tableau.cpp.o
- [ 32%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/tableau_sizes.cpp.o
- [ 32%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/soi_simplex.cpp.o
- [ 32%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/theory_arith_private.cpp.o
- [ 32%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/coverings_solver.cpp.o
- [ 33%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/coverings/cdcac_utils.cpp.o
- [ 33%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/coverings/cdcac.cpp.o
- [ 33%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/coverings/cocoa_converter.cpp.o
- [ 33%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/coverings/lazard_evaluation.cpp.o
- [ 33%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/coverings/projections.cpp.o
- [ 33%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/coverings/proof_checker.cpp.o
- [ 33%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/coverings/constraints.cpp.o
- [ 33%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/coverings/proof_generator.cpp.o
- [ 33%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/equality_substitution.cpp.o
- [ 33%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/ext/arith_nl_compare_proof_gen.cpp.o
- [ 34%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/ext/constraint.cpp.o
- [ 34%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/ext/factoring_check.cpp.o
- [ 34%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/ext/monomial_check.cpp.o
- [ 34%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/coverings/variable_ordering.cpp.o
- [ 34%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/ext/monomial_bounds_check.cpp.o
- [ 34%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/ext/ext_state.cpp.o
- [ 34%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/ext/proof_checker.cpp.o
- [ 34%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/ext/split_zero_check.cpp.o
- [ 34%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/ext/monomial.cpp.o
- [ 34%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/ext/tangent_plane_check.cpp.o
- [ 34%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/ext_theory_callback.cpp.o
- [ 35%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/iand_solver.cpp.o
- [ 35%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/icp/candidate.cpp.o
- [ 35%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/icp/icp_solver.cpp.o
- [ 35%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/icp/contraction_origins.cpp.o
- [ 35%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/icp/intersection.cpp.o
- [ 35%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/iand_utils.cpp.o
- [ 35%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/nl_lemma_utils.cpp.o
- [ 35%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/nonlinear_extension.cpp.o
- [ 35%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/poly_conversion.cpp.o
- [ 36%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/pow2_solver.cpp.o
- [ 36%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/nl_model.cpp.o
- [ 36%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/stats.cpp.o
- [ 36%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/transcendental/exponential_solver.cpp.o
- [ 36%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/strategy.cpp.o
- [ 36%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/transcendental/proof_checker.cpp.o
- [ 36%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/transcendental/sine_solver.cpp.o
- [ 36%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/transcendental/transcendental_solver.cpp.o
- [ 36%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/transcendental/taylor_generator.cpp.o
- [ 36%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/transcendental/transcendental_state.cpp.o
- [ 36%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/operator_elim.cpp.o
- [ 38%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/pp_rewrite_eq.cpp.o
- [ 38%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/rewriter/addition.cpp.o
- [ 38%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/proof_checker.cpp.o
- [ 38%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/rewriter/node_utils.cpp.o
- [ 38%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/rewriter/rewrite_atom.cpp.o
- [ 38%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/rewrites.cpp.o
- [ 38%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/theory_arith.cpp.o
- [ 38%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/theory_arith_type_rules.cpp.o
- [ 38%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arrays/array_info.cpp.o
- [ 38%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arrays/proof_checker.cpp.o
- [ 39%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arrays/inference_manager.cpp.o
- make: Leaving directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build'
- [WARNING] OPAMCONFIRMLEVEL was ignored because CLI 2.0 was requested and it was introduced in 2.1.
- fatal: not a git repository: /home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/../../.git/modules/vendor/cvc5
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/parser/CMakeFiles/cvc5parser-objs.dir/build.make:79: src/parser/CMakeFiles/cvc5parser-objs.dir/commands.cpp.o] Error 1
- make[2]: *** Waiting for unfinished jobs....
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/parser/CMakeFiles/cvc5parser-objs.dir/build.make:191: src/parser/CMakeFiles/cvc5parser-objs.dir/smt2/smt2_state.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/parser/CMakeFiles/cvc5parser-objs.dir/build.make:205: src/parser/CMakeFiles/cvc5parser-objs.dir/smt2/smt2_cmd_parser.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:107: src/CMakeFiles/cvc5-obj.dir/api/cpp/cvc5.cpp.o] Error 1
- make[2]: *** Waiting for unfinished jobs....
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/parser/CMakeFiles/cvc5parser-objs.dir/build.make:247: src/parser/CMakeFiles/cvc5parser-objs.dir/smt2/smt2_term_parser.cpp.o] Error 1
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:471: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/bv_to_int.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:429: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/bv_gauss.cpp.o] Error 1
- make[1]: *** [CMakeFiles/Makefile2:1138: src/parser/CMakeFiles/cvc5parser-objs.dir/all] Error 2
- make[1]: *** Waiting for unfinished jobs....
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:415: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/bv_eager_atoms.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:401: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/bool_to_bv.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:219: src/CMakeFiles/cvc5-obj.dir/decision/justify_stack.cpp.o] Error 1
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:457: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/bv_to_bool.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:583: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/int_to_bv.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:205: src/CMakeFiles/cvc5-obj.dir/decision/justify_info.cpp.o] Error 1
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:149: src/CMakeFiles/cvc5-obj.dir/decision/assertion_list.cpp.o] Error 1
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:163: src/CMakeFiles/cvc5-obj.dir/decision/decision_engine.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:373: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/ackermann.cpp.o] Error 1
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:443: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/bv_intro_pow2.cpp.o] Error 1
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:611: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/ite_simp.cpp.o] Error 1
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:625: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/learned_rewrite.cpp.o] Error 1
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:639: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/miplib_trick.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:79: src/CMakeFiles/cvc5-obj.dir/api/c/cvc5.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:177: src/CMakeFiles/cvc5-obj.dir/decision/justification_strategy.cpp.o] Error 1
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1171: src/CMakeFiles/cvc5-obj.dir/proof/lazy_proof_chain.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:541: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/fun_def_fmf.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:485: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/extended_rewriter_pass.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:387: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/apply_substs.cpp.o] Error 1
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:779: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/static_rewrite.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:345: src/CMakeFiles/cvc5-obj.dir/preprocessing/assertion_pipeline.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:667: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/non_clausal_simp.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:527: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/foreign_theory_rewrite.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:653: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/nl_ext_purify.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:93: src/CMakeFiles/cvc5-obj.dir/api/c/cvc5_c_structs.cpp.o] Error 1
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:331: src/CMakeFiles/cvc5-obj.dir/options/options_handler.cpp.o] Error 1
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:597: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/ite_removal.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:191: src/CMakeFiles/cvc5-obj.dir/decision/justify_cache.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:359: src/CMakeFiles/cvc5-obj.dir/preprocessing/learned_literal_manager.cpp.o] Error 1
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:513: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/ff_disjunctive_bit.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:737: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/sep_skolem_emp.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:877: src/CMakeFiles/cvc5-obj.dir/preprocessing/preprocessing_pass_context.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:709: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/real_to_int.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:569: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/ho_elim.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:989: src/CMakeFiles/cvc5-obj.dir/printer/smt2/smt2_printer.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1087: src/CMakeFiles/cvc5-obj.dir/proof/buffered_proof_generator.cpp.o] Error 1
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:821: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/synth_rew_rules.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:555: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/global_negate.cpp.o] Error 1
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:751: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/sort_infer.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:905: src/CMakeFiles/cvc5-obj.dir/preprocessing/util/boolean_simplification.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:499: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/ff_bitsum.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:849: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/unconstrained_simplifier.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:835: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/theory_preprocess.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:681: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/pseudo_boolean_processor.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1017: src/CMakeFiles/cvc5-obj.dir/proof/alf/alf_list_node_converter.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:765: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/static_learning.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:919: src/CMakeFiles/cvc5-obj.dir/preprocessing/util/ite_utilities.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1199: src/CMakeFiles/cvc5-obj.dir/proof/lfsc/lfsc_list_sc_node_converter.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1493: src/CMakeFiles/cvc5-obj.dir/proof/resolution_proofs_util.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:807: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/sygus_inference.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1101: src/CMakeFiles/cvc5-obj.dir/proof/conv_proof_generator.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1045: src/CMakeFiles/cvc5-obj.dir/proof/alf/alf_print_channel.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1003: src/CMakeFiles/cvc5-obj.dir/proof/alf/alf_dependent_type_converter.cpp.o] Error 1
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1115: src/CMakeFiles/cvc5-obj.dir/proof/conv_seq_proof_generator.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:961: src/CMakeFiles/cvc5-obj.dir/printer/let_binding.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1241: src/CMakeFiles/cvc5-obj.dir/proof/lfsc/lfsc_printer.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:863: src/CMakeFiles/cvc5-obj.dir/preprocessing/preprocessing_pass.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:891: src/CMakeFiles/cvc5-obj.dir/preprocessing/preprocessing_pass_registry.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:975: src/CMakeFiles/cvc5-obj.dir/printer/printer.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1227: src/CMakeFiles/cvc5-obj.dir/proof/lfsc/lfsc_post_processor.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1367: src/CMakeFiles/cvc5-obj.dir/proof/proof_letify.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1269: src/CMakeFiles/cvc5-obj.dir/proof/lfsc/lfsc_util.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1843: src/CMakeFiles/cvc5-obj.dir/prop/proof_cnf_stream.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1521: src/CMakeFiles/cvc5-obj.dir/proof/subtype_elim_proof_converter.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1787: src/CMakeFiles/cvc5-obj.dir/prop/minisat/minisat.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1647: src/CMakeFiles/cvc5-obj.dir/proof/alethe/alethe_post_processor.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1605: src/CMakeFiles/cvc5-obj.dir/proof/valid_witness_proof_generator.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2011: src/CMakeFiles/cvc5-obj.dir/smt/check_models.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2235: src/CMakeFiles/cvc5-obj.dir/smt/print_benchmark.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2613: src/CMakeFiles/cvc5-obj.dir/theory/arith/arith_rewriter.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:3005: src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/soi_simplex.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2599: src/CMakeFiles/cvc5-obj.dir/theory/arith/arith_proof_utilities.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1577: src/CMakeFiles/cvc5-obj.dir/proof/theory_proof_step_buffer.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1129: src/CMakeFiles/cvc5-obj.dir/proof/dot/dot_printer.cpp.o] Error 1
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2025: src/CMakeFiles/cvc5-obj.dir/smt/context_manager.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1381: src/CMakeFiles/cvc5-obj.dir/proof/proof_node.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1031: src/CMakeFiles/cvc5-obj.dir/proof/alf/alf_node_converter.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1689: src/CMakeFiles/cvc5-obj.dir/prop/cadical.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1955: src/CMakeFiles/cvc5-obj.dir/prop/theory_proxy.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1409: src/CMakeFiles/cvc5-obj.dir/proof/proof_node_converter.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1059: src/CMakeFiles/cvc5-obj.dir/proof/alf/alf_printer.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:695: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/quantifiers_preprocess.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1885: src/CMakeFiles/cvc5-obj.dir/prop/prop_proof_manager.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1395: src/CMakeFiles/cvc5-obj.dir/proof/proof_node_algorithm.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1871: src/CMakeFiles/cvc5-obj.dir/prop/prop_engine.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2109: src/CMakeFiles/cvc5-obj.dir/smt/listeners.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1829: src/CMakeFiles/cvc5-obj.dir/prop/minisat/simp/SimpSolver.cc.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2977: src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/simplex.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1633: src/CMakeFiles/cvc5-obj.dir/proof/alethe/alethe_node_converter.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2095: src/CMakeFiles/cvc5-obj.dir/smt/find_synth_solver.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2445: src/CMakeFiles/cvc5-obj.dir/smt/sygus_solver.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2641: src/CMakeFiles/cvc5-obj.dir/theory/arith/arith_utilities.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2473: src/CMakeFiles/cvc5-obj.dir/smt/timeout_core_manager.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2263: src/CMakeFiles/cvc5-obj.dir/smt/proof_manager.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1983: src/CMakeFiles/cvc5-obj.dir/smt/abduction_solver.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1437: src/CMakeFiles/cvc5-obj.dir/proof/proof_node_manager.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2207: src/CMakeFiles/cvc5-obj.dir/smt/preprocessor.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2039: src/CMakeFiles/cvc5-obj.dir/smt/difficulty_post_processor.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1969: src/CMakeFiles/cvc5-obj.dir/prop/zero_level_learner.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1661: src/CMakeFiles/cvc5-obj.dir/proof/alethe/alethe_printer.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1997: src/CMakeFiles/cvc5-obj.dir/smt/assertions.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2487: src/CMakeFiles/cvc5-obj.dir/smt/unsat_core_manager.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1703: src/CMakeFiles/cvc5-obj.dir/prop/cnf_stream.cpp.o] Error 1
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2067: src/CMakeFiles/cvc5-obj.dir/smt/env_obj.cpp.o] Error 1
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2319: src/CMakeFiles/cvc5-obj.dir/smt/proof_post_processor_dsl.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2123: src/CMakeFiles/cvc5-obj.dir/smt/illegal_checker.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2193: src/CMakeFiles/cvc5-obj.dir/smt/quant_elim_solver.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1899: src/CMakeFiles/cvc5-obj.dir/prop/sat_solver_factory.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2081: src/CMakeFiles/cvc5-obj.dir/smt/expand_definitions.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1773: src/CMakeFiles/cvc5-obj.dir/prop/minisat/core/Solver.cc.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1213: src/CMakeFiles/cvc5-obj.dir/proof/lfsc/lfsc_node_converter.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2851: src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/dual_simplex.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2053: src/CMakeFiles/cvc5-obj.dir/smt/env.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2137: src/CMakeFiles/cvc5-obj.dir/smt/interpolation_solver.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2389: src/CMakeFiles/cvc5-obj.dir/smt/smt_driver.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2403: src/CMakeFiles/cvc5-obj.dir/smt/smt_driver_deep_restarts.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2277: src/CMakeFiles/cvc5-obj.dir/smt/proof_final_callback.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1815: src/CMakeFiles/cvc5-obj.dir/prop/minisat/sat_proof_manager.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2655: src/CMakeFiles/cvc5-obj.dir/theory/arith/bound_inference.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1941: src/CMakeFiles/cvc5-obj.dir/prop/theory_preregistrar.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2949: src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/normal_form.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1451: src/CMakeFiles/cvc5-obj.dir/proof/proof_node_updater.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:793: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/strings_eager_pp.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2809: src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/constraint.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2529: src/CMakeFiles/cvc5-obj.dir/theory/arith/arith_ite_utils.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2249: src/CMakeFiles/cvc5-obj.dir/smt/process_assertions.cpp.o] Error 1
- c++: fatal error: Killed signal terminated program cc1plus
- compilation terminated.
- make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2781: src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/callbacks.cpp.o] Error 1
- make[1]: *** [CMakeFiles/Makefile2:934: src/CMakeFiles/cvc5-obj.dir/all] Error 2
- make: *** [Makefile:146: all] Error 2
[ERROR] The compilation of cvc5.1.3.0-1 failed at "dune build -p cvc5 -j 255 @install".
build failed...
Dependency Graph
Loading graph...
View raw DOT format
digraph opam {
"conf-python3-pyparsing.1" -> "conf-python-3.9.0.0";
"conf-python3-tomli.1" -> "conf-python-3.9.0.0";
"cvc5.1.3.0-1" -> {"conf-cmake.1" "conf-g++.1.0" "conf-gcc.1.0" "conf-gmp.5" "conf-python-3.9.0.0" "conf-python-3-dev.1" "conf-python3-pyparsing.1" "conf-python3-tomli.1" "dune.3.20.2" "ocaml.5.4.0"}
"dune.3.20.2" -> {"base-threads.base" "base-unix.base" "ocaml.5.4.0"}
"ocaml.5.4.0" -> {"ocaml-base-compiler.5.4.0" "ocaml-config.3"}
"ocaml-base-compiler.5.4.0" -> "ocaml-compiler.5.4.0";
"ocaml-config.3" -> "ocaml-base-compiler.5.4.0";
}