Build Log: cvc5.1.3.0-1

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/static_pic_poly.dir/utils/output.c.o - [ 0%] Building C object src/CMakeFiles/static_pic_poly.dir/utils/assignment.c.o - [ 1%] Building C object src/CMakeFiles/static_pic_poly.dir/utils/sign_condition.c.o - [ 1%] Building C object src/CMakeFiles/static_pic_poly.dir/utils/u_memstream.c.o - [ 2%] Building C object src/CMakeFiles/static_pic_poly.dir/number/integer.c.o - [ 3%] Building C object src/CMakeFiles/static_pic_poly.dir/number/dyadic_rational.c.o - [ 3%] Building C object src/CMakeFiles/static_pic_poly.dir/number/algebraic_number.c.o - [ 3%] Building C object src/CMakeFiles/static_pic_poly.dir/number/rational.c.o - [ 4%] Building C object src/CMakeFiles/poly.dir/utils/assignment.c.o - [ 5%] Building C object src/CMakeFiles/static_pic_poly.dir/number/value.c.o - [ 5%] Building C object src/CMakeFiles/static_pic_poly.dir/interval/arithmetic.c.o - [ 5%] Building C object src/CMakeFiles/static_pic_poly.dir/utils/debug_trace.c.o - [ 5%] Building C object src/CMakeFiles/static_pic_poly.dir/interval/interval.c.o - [ 5%] Building C object src/CMakeFiles/static_pic_poly.dir/variable/variable_db.c.o - [ 5%] Building C object src/CMakeFiles/poly.dir/utils/debug_trace.c.o - [ 8%] Building C object src/CMakeFiles/static_poly.dir/utils/debug_trace.c.o - [ 9%] Building C object src/CMakeFiles/poly.dir/utils/sign_condition.c.o - [ 10%] Building C object src/CMakeFiles/static_pic_poly.dir/variable/variable_order.c.o - [ 11%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/upolynomial.c.o - [ 11%] Building C object src/CMakeFiles/static_pic_poly.dir/utils/statistics.c.o - [ 6%] Building C object src/CMakeFiles/static_poly.dir/utils/assignment.c.o - [ 7%] Building C object src/CMakeFiles/poly.dir/utils/statistics.c.o - [ 11%] Building C object src/CMakeFiles/poly.dir/utils/u_memstream.c.o - [ 11%] Building C object src/CMakeFiles/static_pic_poly.dir/variable/variable_list.c.o - [ 11%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/umonomial.c.o - [ 11%] Building C object src/CMakeFiles/static_poly.dir/utils/output.c.o - [ 11%] Building C object src/CMakeFiles/poly.dir/utils/output.c.o - [ 11%] Building C object src/CMakeFiles/static_poly.dir/utils/statistics.c.o - [ 12%] Building C object src/CMakeFiles/poly.dir/number/integer.c.o - [ 12%] Building C object src/CMakeFiles/static_poly.dir/utils/u_memstream.c.o - [ 13%] Building C object src/CMakeFiles/poly.dir/number/dyadic_rational.c.o - [ 13%] Building C object src/CMakeFiles/poly.dir/upolynomial/umonomial.c.o - [ 13%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/output.c.o - [ 13%] Building C object src/CMakeFiles/poly.dir/upolynomial/output.c.o - [ 13%] Building C object src/CMakeFiles/static_poly.dir/variable/variable_list.c.o - [ 14%] Building C object src/CMakeFiles/poly.dir/upolynomial/upolynomial.c.o - [ 14%] Building C object src/CMakeFiles/static_poly.dir/variable/variable_db.c.o - [ 15%] Building C object src/CMakeFiles/poly.dir/upolynomial/upolynomial_dense.c.o - [ 16%] Building C object src/CMakeFiles/static_poly.dir/variable/variable_order.c.o - [ 17%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/upolynomial.c.o - [ 17%] Building C object src/CMakeFiles/poly.dir/number/rational.c.o - [ 17%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/umonomial.c.o - [ 17%] Building C object src/CMakeFiles/poly.dir/upolynomial/gcd.c.o - [ 17%] Building C object src/CMakeFiles/poly.dir/upolynomial/bounds.c.o - [ 17%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/output.c.o - [ 17%] Building C object src/CMakeFiles/poly.dir/number/algebraic_number.c.o - [ 24%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/factorization.c.o - [ 25%] Building C object src/CMakeFiles/poly.dir/polynomial/output.c.o - [ 26%] Building C object src/CMakeFiles/static_poly.dir/number/dyadic_rational.c.o - [ 28%] Building C object src/CMakeFiles/poly.dir/interval/interval.c.o - [ 29%] Building C object src/CMakeFiles/static_poly.dir/polynomial/monomial.c.o - [ 30%] Building C object src/CMakeFiles/poly.dir/polynomial/subres.c.o - [ 31%] Building C object src/CMakeFiles/static_poly.dir/polynomial/output.c.o - [ 31%] Building C object src/CMakeFiles/poly.dir/upolynomial/upolynomial_vector.c.o - [ 18%] Building C object src/CMakeFiles/poly.dir/upolynomial/factorization.c.o - [ 31%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/factors.c.o - [ 31%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/root_finding.c.o - [ 19%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/upolynomial_dense.c.o - [ 31%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/bounds.c.o - [ 31%] Building C object src/CMakeFiles/poly.dir/upolynomial/factors.c.o - [ 31%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/upolynomial_vector.c.o - [ 31%] Building C object src/CMakeFiles/static_poly.dir/polynomial/coefficient.c.o - [ 31%] Building C object src/CMakeFiles/poly.dir/polynomial/factorization.c.o - [ 31%] Building C object src/CMakeFiles/static_poly.dir/number/rational.c.o - [ 20%] Building C object src/CMakeFiles/static_poly.dir/number/integer.c.o - [ 31%] Building C object src/CMakeFiles/poly.dir/interval/arithmetic.c.o - [ 32%] Building C object src/CMakeFiles/static_poly.dir/number/value.c.o - [ 34%] Building C object src/CMakeFiles/poly.dir/polynomial/feasibility_set_int.c.o - [ 35%] Building C object src/CMakeFiles/poly.dir/polynomial/polynomial_context.c.o - [ 36%] Building C object src/CMakeFiles/poly.dir/variable/variable_db.c.o - [ 37%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/upolynomial_dense.c.o - [ 38%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/factors.c.o - [ 39%] Building C object src/CMakeFiles/static_poly.dir/polynomial/polynomial.c.o - [ 40%] Building C object src/CMakeFiles/poly.dir/variable/variable_order.c.o - [ 41%] Building C object src/CMakeFiles/static_poly.dir/polynomial/feasibility_set.c.o - [ 42%] Building C object src/CMakeFiles/poly.dir/polynomial/polynomial_heap.c.o - [ 43%] Building C object src/CMakeFiles/static_poly.dir/interval/arithmetic.c.o - [ 44%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/subres.c.o - [ 45%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/root_finding.c.o - [ 46%] Building C object src/CMakeFiles/poly.dir/poly.c.o - [ 47%] 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_context.c.o - [ 49%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/polynomial_heap.c.o - [ 51%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/monomial.c.o - [ 51%] Building C object src/CMakeFiles/static_poly.dir/poly.c.o - [ 31%] Building C object src/CMakeFiles/poly.dir/polynomial/gcd.c.o - [ 52%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/gcd.c.o - [ 52%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/gcd.c.o - [ 27%] Building C object src/CMakeFiles/poly.dir/polynomial/monomial.c.o - [ 22%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/gcd.c.o - [ 52%] Building C object src/CMakeFiles/poly.dir/polynomial/polynomial_vector.c.o - [ 52%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/polynomial_hash_set.c.o - [ 52%] Building C object src/CMakeFiles/poly.dir/polynomial/polynomial_hash_set.c.o - [ 52%] Building C object src/CMakeFiles/static_poly.dir/polynomial/feasibility_set_int.c.o - [ 52%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/polynomial.c.o - [ 52%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/factorization.c.o - [ 52%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/coefficient.c.o - [ 52%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/polynomial_vector.c.o - [ 52%] Building C object src/CMakeFiles/static_poly.dir/utils/sign_condition.c.o - [ 52%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/upolynomial_vector.c.o - [ 31%] Building C object src/CMakeFiles/poly.dir/polynomial/coefficient.c.o - [ 52%] Building C object src/CMakeFiles/static_poly.dir/interval/interval.c.o - [ 52%] Building C object src/CMakeFiles/static_poly.dir/polynomial/polynomial_hash_set.c.o - [ 52%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/factorization.c.o - [ 52%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/feasibility_set.c.o - [ 52%] Building C object src/CMakeFiles/static_poly.dir/polynomial/polynomial_vector.c.o - [ 52%] Building C object src/CMakeFiles/poly.dir/polynomial/feasibility_set.c.o - [ 23%] Building C object src/CMakeFiles/poly.dir/upolynomial/root_finding.c.o - [ 52%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/bounds.c.o - [ 52%] Building C object src/CMakeFiles/static_poly.dir/polynomial/factorization.c.o - [ 52%] Building C object src/CMakeFiles/static_poly.dir/polynomial/gcd.c.o - [ 52%] Building C object src/CMakeFiles/poly.dir/polynomial/polynomial.c.o - [ 52%] Building C object src/CMakeFiles/static_poly.dir/number/algebraic_number.c.o - [ 52%] Building C object src/CMakeFiles/static_poly.dir/polynomial/polynomial_context.c.o - [ 21%] Building C object src/CMakeFiles/poly.dir/number/value.c.o - [ 53%] Building C object src/CMakeFiles/static_poly.dir/polynomial/polynomial_heap.c.o - [ 54%] Building C object src/CMakeFiles/static_pic_poly.dir/poly.c.o - [ 33%] Building C object src/CMakeFiles/static_poly.dir/polynomial/subres.c.o - [ 54%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/output.c.o - [ 54%] Building C object src/CMakeFiles/poly.dir/variable/variable_list.c.o - [ 54%] Linking C static library libpoly.a - [ 54%] Linking C static library libpicpoly.a - [ 54%] Built target static_poly - [ 54%] Linking C shared library libpoly.so - [ 54%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/assignment.cpp.o - [ 54%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/dyadic_rational.cpp.o - [ 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/integer.cpp.o - [ 56%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/dyadic_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 - [ 58%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/interval.cpp.o - [ 59%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/polynomial.cpp.o - [ 59%] Built target static_pic_poly - [ 60%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/rational.cpp.o - [ 60%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/polynomial_utils.cpp.o - [ 60%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/upolynomial.cpp.o - [ 61%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/rational_interval.cpp.o - [ 62%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/utils.cpp.o - [ 62%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/sign_condition.cpp.o - [ 62%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/value.cpp.o - [ 62%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/variable.cpp.o - [ 63%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/algebraic_number.cpp.o - [ 63%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/assignment.cpp.o - [ 63%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/context.cpp.o - [ 64%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/dyadic_interval.cpp.o - [ 65%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/interval_assignment.cpp.o - [ 66%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/integer_ring.cpp.o - [ 66%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/integer.cpp.o - [ 66%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/dyadic_rational.cpp.o - [ 66%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/interval.cpp.o - [ 67%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/polynomial.cpp.o - [ 68%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/polynomial_utils.cpp.o - [ 68%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/rational.cpp.o - [ 68%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/rational_interval.cpp.o - [ 68%] Built target poly - [ 68%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/sign_condition.cpp.o - [ 69%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/upolynomial.cpp.o - [ 69%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/utils.cpp.o - [ 70%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/value.cpp.o - [ 70%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/variable.cpp.o - [ 71%] Building C object python/CMakeFiles/polypy.dir/polypyAlgebraicNumber.c.o - [ 72%] Building C object python/CMakeFiles/polypy.dir/polypyAssignment.c.o - [ 73%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/algebraic_number.cpp.o - [ 72%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/assignment.cpp.o - [ 73%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/dyadic_interval.cpp.o - [ 73%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/dyadic_rational.cpp.o - [ 73%] Building C object python/CMakeFiles/polypy.dir/polypyInteger.c.o - [ 74%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/integer_ring.cpp.o - [ 74%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/context.cpp.o - [ 74%] Building C object python/CMakeFiles/polypy.dir/polypy.c.o - [ 75%] Building C object python/CMakeFiles/polypy.dir/polypyPolynomial.c.o - [ 76%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/interval_assignment.cpp.o - [ 76%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/interval.cpp.o - [ 76%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/polynomial.cpp.o - [ 77%] Building C object python/CMakeFiles/polypy.dir/polypyVariableOrder.c.o - [ 77%] Building C object python/CMakeFiles/polypy.dir/polypyVariable.c.o - [ 78%] Building C object python/CMakeFiles/polypy.dir/polypyValue.c.o - [ 78%] Building C object python/CMakeFiles/polypy.dir/utils.c.o - [ 78%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/integer.cpp.o - [ 78%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/rational.cpp.o - [ 79%] Building C object python/CMakeFiles/polypy.dir/polypyUPolynomial.c.o - [ 79%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/sign_condition.cpp.o - [ 79%] Building C object python/CMakeFiles/polypy.dir/polypyFeasibilitySet.c.o - [ 79%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/utils.cpp.o - [ 80%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/upolynomial.cpp.o - [ 81%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/polynomial_utils.cpp.o - [ 79%] Building C object python/CMakeFiles/polypy.dir/polypyInterval.c.o - [ 82%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/rational_interval.cpp.o - [ 83%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/value.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 static library libpicpolyxx.a - [ 86%] Built target static_polyxx - [ 87%] Linking CXX shared library libpolyxx.so - [ 87%] Built target static_pic_polyxx - [ 87%] Built target polyxx - [ 89%] Building CXX object test/polyxx/CMakeFiles/test_dyadic_interval.dir/test_dyadic_interval.cpp.o - [ 90%] Building CXX object test/polyxx/CMakeFiles/test_integer.dir/test_integer.cpp.o - [ 90%] Building CXX object test/poly/CMakeFiles/test_feasible_int_set.dir/test_feasible_int_set.cpp.o - [ 88%] Building CXX object test/polyxx/CMakeFiles/test_interval.dir/test_interval.cpp.o - [ 91%] Building CXX object test/polyxx/CMakeFiles/test_interval_assignment.dir/test_interval_assignment.cpp.o - [ 91%] Building CXX object test/polyxx/CMakeFiles/test_algebraic_number.dir/test_algebraic_number.cpp.o - [ 91%] Building CXX object test/polyxx/CMakeFiles/test_assignment.dir/test_assignment.cpp.o - [ 91%] Building CXX object test/polyxx/CMakeFiles/test_dyadic_rational.dir/test_dyadic_rational.cpp.o - [ 92%] Building CXX object test/polyxx/CMakeFiles/test_polynomial.dir/test_polynomial.cpp.o - [ 92%] Building CXX object test/polyxx/CMakeFiles/test_upolynomial.dir/test_upolynomial.cpp.o - [ 92%] Building CXX object test/polyxx/CMakeFiles/test_rational.dir/test_rational.cpp.o - [ 92%] Building CXX object test/polyxx/CMakeFiles/test_value.dir/test_value.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 - [ 93%] Linking CXX executable test_variable - [ 94%] Linking CXX executable test_assignment - [ 94%] Linking CXX executable test_interval_assignment - [ 95%] Linking CXX executable test_rational_interval - [ 95%] Linking CXX executable test_polynomial - [ 96%] Linking CXX executable test_algebraic_number - [ 96%] Built target test_variable - [ 97%] Linking CXX executable test_dyadic_interval - [ 97%] Built target test_assignment - [ 97%] Built target test_interval_assignment - [ 97%] Built target test_rational_interval - [ 98%] Linking CXX executable test_rational - [ 98%] Built target test_polynomial - [ 98%] Linking CXX executable test_integer - [ 98%] Built target test_dyadic_interval - [ 98%] Linking CXX executable test_dyadic_rational - [ 98%] Built target test_algebraic_number - [ 98%] Linking CXX executable test_interval - [ 98%] Linking CXX executable test_feasible_int_set - [ 99%] Linking CXX executable test_upolynomial - [ 99%] Built target test_rational - [100%] Linking CXX executable test_value - [100%] Built target test_integer - [100%] Built target test_dyadic_rational - [100%] Built target test_feasible_int_set - [100%] Built target test_upolynomial - [100%] Built target test_interval - [100%] Built target test_value - [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 (8.6s) - -- Generating done (0.6s) - -- 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' - [ 0%] Generating options/options.stamp - [ 0%] Generating theory_traits.h - [ 0%] Generating rewriter_tables.h - [ 0%] Generating type_enumerator.cpp - [ 0%] Building CXX object src/context/CMakeFiles/cvc5context.dir/context.cpp.o - [ 1%] Generating node_manager.h - -- Found Git: /usr/bin/git (found version "2.47.3") - [ 1%] Building CXX object src/context/CMakeFiles/cvc5context.dir/context_mm.cpp.o - [ 1%] Generating kind.h - [ 2%] Generating smt2_tokens.h - [ 2%] Generating type_properties.h - [ 2%] Generating rewrites.{h,cpp} - [ 2%] Generating metakind.h - [ 2%] Generating type_checker.cpp - [ 2%] Built target gen-versioninfo - [ 2%] Generating Trace_tags.h - [ 2%] Built target gen-tokens - [ 2%] Generating node_manager.cpp - [ 2%] Built target gen-theory - [ 2%] Generating type_properties.cpp - [ 2%] Generating metakind.cpp - [ 2%] Generating kind.cpp - [ 2%] Built target gen-options - [ 2%] Built target gen-expr - [ 2%] Built target gen-tags - [ 2%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/command_status.cpp.o - [ 2%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/commands.cpp.o - [ 2%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/input.cpp.o - [ 3%] Building CXX object src/base/CMakeFiles/cvc5base.dir/check.cpp.o - [ 3%] Building CXX object src/base/CMakeFiles/cvc5base.dir/configuration.cpp.o - [ 3%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/lexer.cpp.o - [ 3%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/parser.cpp.o - [ 3%] Building CXX object src/base/CMakeFiles/cvc5base.dir/output.cpp.o - [ 3%] Building CXX object src/base/CMakeFiles/cvc5base.dir/exception.cpp.o - [ 4%] Building CXX object src/base/CMakeFiles/cvc5base.dir/listener.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/base/CMakeFiles/cvc5base.dir/versioninfo.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_lexer.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_term_parser.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/sym_manager.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 - [ 5%] Building CXX object src/CMakeFiles/cvc5-obj.dir/api/cpp/cvc5_types.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/decision/decision_engine.cpp.o - [ 7%] Building CXX object src/CMakeFiles/cvc5-obj.dir/api/cpp/cvc5.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/assertion_list.cpp.o - [ 7%] Building CXX object src/CMakeFiles/cvc5-obj.dir/decision/justification_strategy.cpp.o - [ 7%] Building CXX object src/CMakeFiles/cvc5-obj.dir/decision/justify_cache.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/decision/justify_stack.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 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/options/options_handler.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/options/managed_streams.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_gauss.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_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 - [ 10%] 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/fun_def_fmf.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/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 - [ 10%] 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/real_to_int.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/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/theory_preprocess.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/preprocessing_pass.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_registry.cpp.o - [ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/preprocessing_pass_context.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/ast/ast_printer.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/printer/smt2/smt2_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/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/eager_proof_generator.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/lfsc/lfsc_post_processor.cpp.o - [ 15%] 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/lazy_tree_proof_generator.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_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/method_id.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/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_generator.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_node_converter.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_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_node_algorithm.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_step_buffer.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/resolution_proofs_util.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/subtype_elim_proof_converter.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/trust_node.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 - [ 21%] 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/theory_preregistrar.cpp.o - [ 22%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/theory_proxy.cpp.o - [ 22%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/zero_level_learner.cpp.o - [ 22%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/abduction_solver.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/smt/env.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/difficulty_post_processor.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/expand_definitions.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/model.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_core_builder.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/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 - [ 25%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/proof_logger.cpp.o - [ 25%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/proof_post_processor.cpp.o - [ 25%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/proof_manager.cpp.o - [ 25%] 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/proof_final_callback.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/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/smt_driver.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_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/smt_solver.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/term_formula_removal.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/timeout_core_manager.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_poly_norm.cpp.o - [ 28%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/witness_form.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_preprocess.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/arith_proof_utilities.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_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/branch_and_bound.cpp.o - [ 28%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/bound_inference.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/callbacks.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/constraint.cpp.o - [ 29%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/congruence_manager.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/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/dio_solver.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/matrix.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/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/soi_simplex.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/tableau.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 - [ 32%] 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/cdcac_utils.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/constraints.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/proof_checker.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/coverings/projections.cpp.o - [ 33%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/coverings/variable_ordering.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 - [ 33%] 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/constraint.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/monomial_bounds_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/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/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/contraction_origins.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/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/nl_model.cpp.o - [ 35%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/nonlinear_extension.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/stats.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/poly_conversion.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/transcendental/sine_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/proof_checker.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/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/proof_checker.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/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 - [ 39%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arrays/inference_manager.cpp.o - [ 39%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arrays/proof_checker.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: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/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:247: src/parser/CMakeFiles/cvc5parser-objs.dir/smt2/smt2_term_parser.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:107: src/CMakeFiles/cvc5-obj.dir/api/cpp/cvc5.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** Waiting for unfinished jobs.... - 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:149: src/CMakeFiles/cvc5-obj.dir/decision/assertion_list.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 - 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:177: src/CMakeFiles/cvc5-obj.dir/decision/justification_strategy.cpp.o] Error 1 - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:205: src/CMakeFiles/cvc5-obj.dir/decision/justify_info.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - 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. - 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: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:93: src/CMakeFiles/cvc5-obj.dir/api/c/cvc5_c_structs.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. - 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 - 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:429: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/bv_gauss.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 - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:541: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/fun_def_fmf.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. - 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. - 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 - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:527: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/foreign_theory_rewrite.cpp.o] Error 1 - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:583: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/int_to_bv.cpp.o] Error 1 - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:667: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/non_clausal_simp.cpp.o] Error 1 - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:737: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/sep_skolem_emp.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. - 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:373: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/ackermann.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - 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:989: src/CMakeFiles/cvc5-obj.dir/printer/smt2/smt2_printer.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:331: src/CMakeFiles/cvc5-obj.dir/options/options_handler.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:611: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/ite_simp.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - 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. - 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: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: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: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: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: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:933: src/CMakeFiles/cvc5-obj.dir/printer/ast/ast_printer.cpp.o] Error 1 - 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 - 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: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:555: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/global_negate.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: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: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:723: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/rewrite.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:1283: src/CMakeFiles/cvc5-obj.dir/proof/method_id.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: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:1255: src/CMakeFiles/cvc5-obj.dir/proof/lfsc/lfsc_print_channel.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: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: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. - 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:765: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/static_learning.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:1213: src/CMakeFiles/cvc5-obj.dir/proof/lfsc/lfsc_node_converter.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 - 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:219: src/CMakeFiles/cvc5-obj.dir/decision/justify_stack.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: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:1157: src/CMakeFiles/cvc5-obj.dir/proof/lazy_proof.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:1353: src/CMakeFiles/cvc5-obj.dir/proof/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: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: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. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1087: src/CMakeFiles/cvc5-obj.dir/proof/buffered_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:1143: src/CMakeFiles/cvc5-obj.dir/proof/eager_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: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: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:1591: src/CMakeFiles/cvc5-obj.dir/proof/unsat_core.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1759: src/CMakeFiles/cvc5-obj.dir/prop/lemma_inprocess.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1479: src/CMakeFiles/cvc5-obj.dir/proof/proof_step_buffer.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - 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:1325: src/CMakeFiles/cvc5-obj.dir/proof/proof_checker.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:1801: src/CMakeFiles/cvc5-obj.dir/prop/minisat/opt_clauses_manager.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1745: src/CMakeFiles/cvc5-obj.dir/prop/learned_db.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: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: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:2221: src/CMakeFiles/cvc5-obj.dir/smt/preprocess_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:2361: src/CMakeFiles/cvc5-obj.dir/smt/solver_engine_state.cpp.o] Error 1 - 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 - 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: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: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:1185: src/CMakeFiles/cvc5-obj.dir/proof/lazy_tree_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: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. - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1619: src/CMakeFiles/cvc5-obj.dir/proof/alethe/alethe_let_binding.cpp.o] Error 1 - 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:1703: src/CMakeFiles/cvc5-obj.dir/prop/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: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:1857: src/CMakeFiles/cvc5-obj.dir/prop/proof_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: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:2179: src/CMakeFiles/cvc5-obj.dir/smt/model_blocker.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: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:1465: src/CMakeFiles/cvc5-obj.dir/proof/proof_rule_checker.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2585: src/CMakeFiles/cvc5-obj.dir/theory/arith/arith_proof_rcons.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2067: src/CMakeFiles/cvc5-obj.dir/smt/env_obj.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: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: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: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:2823: src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/cut_log.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: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:2347: src/CMakeFiles/cvc5-obj.dir/smt/solver_engine.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:1241: src/CMakeFiles/cvc5-obj.dir/proof/lfsc/lfsc_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:2529: src/CMakeFiles/cvc5-obj.dir/theory/arith/arith_ite_utils.cpp.o] Error 1 - 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:1311: src/CMakeFiles/cvc5-obj.dir/proof/proof.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1507: src/CMakeFiles/cvc5-obj.dir/proof/rewrite_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:2515: src/CMakeFiles/cvc5-obj.dir/theory/arith/arith_evaluator.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2921: src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/linear_equality.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: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: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:2879: src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/fc_simplex.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:2291: src/CMakeFiles/cvc5-obj.dir/smt/proof_logger.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: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: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: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: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:2697: src/CMakeFiles/cvc5-obj.dir/theory/arith/equality_solver.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:2739: src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/arith_static_learner.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: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: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:2487: src/CMakeFiles/cvc5-obj.dir/smt/unsat_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:2711: src/CMakeFiles/cvc5-obj.dir/theory/arith/inference_manager.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 - 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...