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 13.3.0 - -- The CXX compiler identification is GNU 13.3.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.12.3") - -- Found PythonLibs: /usr/lib/x86_64-linux-gnu/libpython3.12.so (found version "3.12.3") - -- Configuring done (3.1s) - -- 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 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/debug_trace.c.o - [ 0%] Building C object src/CMakeFiles/poly.dir/utils/debug_trace.c.o - [ 1%] Building C object src/CMakeFiles/poly.dir/utils/statistics.c.o - [ 0%] Building C object src/CMakeFiles/static_poly.dir/utils/debug_trace.c.o - [ 1%] Building C object src/CMakeFiles/poly.dir/utils/assignment.c.o - [ 1%] Building C object src/CMakeFiles/static_poly.dir/utils/statistics.c.o - [ 2%] Building C object src/CMakeFiles/static_pic_poly.dir/utils/sign_condition.c.o - [ 2%] Building C object src/CMakeFiles/poly.dir/utils/u_memstream.c.o - [ 3%] Building C object src/CMakeFiles/static_poly.dir/utils/output.c.o - [ 3%] Building C object src/CMakeFiles/static_pic_poly.dir/number/rational.c.o - [ 4%] Building C object src/CMakeFiles/poly.dir/number/dyadic_rational.c.o - [ 5%] Building C object src/CMakeFiles/static_poly.dir/number/rational.c.o - [ 5%] Building C object src/CMakeFiles/static_pic_poly.dir/number/integer.c.o - [ 6%] Building C object src/CMakeFiles/static_poly.dir/number/dyadic_rational.c.o - [ 7%] Building C object src/CMakeFiles/static_poly.dir/number/algebraic_number.c.o - [ 7%] Building C object src/CMakeFiles/static_pic_poly.dir/number/algebraic_number.c.o - [ 7%] Building C object src/CMakeFiles/static_pic_poly.dir/number/dyadic_rational.c.o - [ 7%] Building C object src/CMakeFiles/static_poly.dir/utils/u_memstream.c.o - [ 7%] Building C object src/CMakeFiles/static_poly.dir/number/integer.c.o - [ 7%] Building C object src/CMakeFiles/poly.dir/number/algebraic_number.c.o - [ 8%] Building C object src/CMakeFiles/static_poly.dir/number/value.c.o - [ 8%] Building C object src/CMakeFiles/poly.dir/number/value.c.o - [ 9%] Building C object src/CMakeFiles/static_pic_poly.dir/number/value.c.o - [ 9%] Building C object src/CMakeFiles/static_pic_poly.dir/utils/output.c.o - [ 9%] Building C object src/CMakeFiles/static_pic_poly.dir/interval/interval.c.o - [ 10%] Building C object src/CMakeFiles/static_poly.dir/utils/assignment.c.o - [ 10%] Building C object src/CMakeFiles/static_pic_poly.dir/utils/assignment.c.o - [ 11%] Building C object src/CMakeFiles/static_poly.dir/utils/sign_condition.c.o - [ 11%] Building C object src/CMakeFiles/poly.dir/variable/variable_list.c.o - [ 11%] Building C object src/CMakeFiles/static_poly.dir/variable/variable_db.c.o - [ 11%] Building C object src/CMakeFiles/static_pic_poly.dir/interval/arithmetic.c.o - [ 12%] Building C object src/CMakeFiles/poly.dir/variable/variable_order.c.o - [ 13%] Building C object src/CMakeFiles/static_poly.dir/interval/interval.c.o - [ 14%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/upolynomial_dense.c.o - [ 14%] Building C object src/CMakeFiles/poly.dir/utils/output.c.o - [ 14%] Building C object src/CMakeFiles/poly.dir/upolynomial/gcd.c.o - [ 15%] Building C object src/CMakeFiles/poly.dir/number/integer.c.o - [ 16%] Building C object src/CMakeFiles/poly.dir/utils/sign_condition.c.o - [ 16%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/output.c.o - [ 16%] Building C object src/CMakeFiles/static_pic_poly.dir/utils/u_memstream.c.o - [ 17%] Building C object src/CMakeFiles/static_pic_poly.dir/utils/statistics.c.o - [ 18%] Building C object src/CMakeFiles/poly.dir/upolynomial/upolynomial.c.o - [ 19%] Building C object src/CMakeFiles/poly.dir/upolynomial/factors.c.o - [ 20%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/upolynomial.c.o - [ 20%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/bounds.c.o - [ 20%] Building C object src/CMakeFiles/poly.dir/interval/arithmetic.c.o - [ 21%] Building C object src/CMakeFiles/static_poly.dir/variable/variable_order.c.o - [ 22%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/gcd.c.o - [ 22%] Building C object src/CMakeFiles/poly.dir/upolynomial/factorization.c.o - [ 22%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/factors.c.o - [ 23%] Building C object src/CMakeFiles/poly.dir/upolynomial/bounds.c.o - [ 12%] Building C object src/CMakeFiles/poly.dir/upolynomial/output.c.o - [ 23%] Building C object src/CMakeFiles/poly.dir/upolynomial/umonomial.c.o - [ 23%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/umonomial.c.o - [ 23%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/factorization.c.o - [ 24%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/gcd.c.o - [ 24%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/upolynomial_vector.c.o - [ 25%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/upolynomial.c.o - [ 26%] Building C object src/CMakeFiles/static_poly.dir/variable/variable_list.c.o - [ 26%] Building C object src/CMakeFiles/static_pic_poly.dir/variable/variable_order.c.o - [ 28%] Building C object src/CMakeFiles/static_pic_poly.dir/variable/variable_db.c.o - [ 28%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/umonomial.c.o - [ 28%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/output.c.o - [ 29%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/factorization.c.o - [ 29%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/upolynomial_vector.c.o - [ 29%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/root_finding.c.o - [ 30%] Building C object src/CMakeFiles/poly.dir/upolynomial/root_finding.c.o - [ 30%] Building C object src/CMakeFiles/poly.dir/upolynomial/upolynomial_vector.c.o - [ 30%] Building C object src/CMakeFiles/static_poly.dir/interval/arithmetic.c.o - [ 31%] Building C object src/CMakeFiles/static_poly.dir/polynomial/monomial.c.o - [ 31%] Building C object src/CMakeFiles/poly.dir/interval/interval.c.o - [ 32%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/monomial.c.o - [ 32%] Building C object src/CMakeFiles/poly.dir/polynomial/coefficient.c.o - [ 32%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/factors.c.o - [ 33%] Building C object src/CMakeFiles/static_pic_poly.dir/upolynomial/root_finding.c.o - [ 34%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/upolynomial_dense.c.o - [ 35%] Building C object src/CMakeFiles/poly.dir/variable/variable_db.c.o - [ 31%] Building C object src/CMakeFiles/poly.dir/upolynomial/upolynomial_dense.c.o - [ 36%] Building C object src/CMakeFiles/static_poly.dir/upolynomial/bounds.c.o - [ 36%] Building C object src/CMakeFiles/static_pic_poly.dir/variable/variable_list.c.o - [ 36%] Building C object src/CMakeFiles/poly.dir/polynomial/monomial.c.o - [ 36%] Building C object src/CMakeFiles/poly.dir/number/rational.c.o - [ 37%] Building C object src/CMakeFiles/poly.dir/polynomial/output.c.o - [ 37%] Building C object src/CMakeFiles/static_poly.dir/polynomial/coefficient.c.o - [ 38%] Building C object src/CMakeFiles/static_poly.dir/polynomial/output.c.o - [ 39%] Building C object src/CMakeFiles/static_poly.dir/polynomial/subres.c.o - [ 39%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/coefficient.c.o - [ 40%] Building C object src/CMakeFiles/poly.dir/polynomial/subres.c.o - [ 40%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/gcd.c.o - [ 41%] Building C object src/CMakeFiles/poly.dir/polynomial/polynomial_context.c.o - [ 41%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/factorization.c.o - [ 41%] Building C object src/CMakeFiles/poly.dir/polynomial/feasibility_set.c.o - [ 42%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/subres.c.o - [ 42%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/polynomial.c.o - [ 43%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/polynomial_context.c.o - [ 43%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/feasibility_set.c.o - [ 44%] Building C object src/CMakeFiles/poly.dir/polynomial/feasibility_set_int.c.o - [ 44%] Building C object src/CMakeFiles/static_poly.dir/polynomial/factorization.c.o - [ 44%] Building C object src/CMakeFiles/poly.dir/polynomial/polynomial_hash_set.c.o - [ 45%] Building C object src/CMakeFiles/static_poly.dir/polynomial/polynomial.c.o - [ 47%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/output.c.o - [ 47%] Building C object src/CMakeFiles/static_poly.dir/polynomial/polynomial_context.c.o - [ 47%] Building C object src/CMakeFiles/poly.dir/polynomial/factorization.c.o - [ 47%] Building C object src/CMakeFiles/poly.dir/polynomial/gcd.c.o - [ 47%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/polynomial_hash_set.c.o - [ 49%] Building C object src/CMakeFiles/poly.dir/polynomial/polynomial_heap.c.o - [ 49%] Building C object src/CMakeFiles/static_poly.dir/polynomial/feasibility_set.c.o - [ 48%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/feasibility_set_int.c.o - [ 49%] Building C object src/CMakeFiles/static_poly.dir/polynomial/gcd.c.o - [ 50%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/polynomial_heap.c.o - [ 50%] Building C object src/CMakeFiles/poly.dir/polynomial/polynomial.c.o - [ 50%] Building C object src/CMakeFiles/poly.dir/polynomial/polynomial_vector.c.o - [ 50%] Building C object src/CMakeFiles/static_poly.dir/polynomial/feasibility_set_int.c.o - [ 50%] Building C object src/CMakeFiles/static_poly.dir/polynomial/polynomial_hash_set.c.o - [ 51%] Building C object src/CMakeFiles/poly.dir/poly.c.o - [ 52%] Building C object src/CMakeFiles/static_poly.dir/polynomial/polynomial_heap.c.o - [ 52%] Building C object src/CMakeFiles/static_poly.dir/polynomial/polynomial_vector.c.o - [ 53%] Building C object src/CMakeFiles/static_pic_poly.dir/poly.c.o - [ 53%] Building C object src/CMakeFiles/static_pic_poly.dir/polynomial/polynomial_vector.c.o - [ 54%] Building C object src/CMakeFiles/static_poly.dir/poly.c.o - [ 54%] Linking C static library libpicpoly.a - [ 54%] Linking C static library libpoly.a - [ 54%] Linking C shared library libpoly.so - [ 54%] Built target static_pic_poly - [ 55%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/algebraic_number.cpp.o - [ 55%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/context.cpp.o - [ 56%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/dyadic_interval.cpp.o - [ 56%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/dyadic_rational.cpp.o - [ 56%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/assignment.cpp.o - [ 57%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/integer.cpp.o - [ 58%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/integer_ring.cpp.o - [ 57%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/interval_assignment.cpp.o - [ 58%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/interval.cpp.o - [ 59%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/polynomial.cpp.o - [ 59%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/polynomial_utils.cpp.o - [ 60%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/rational.cpp.o - [ 60%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/rational_interval.cpp.o - [ 60%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/utils.cpp.o - [ 60%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/sign_condition.cpp.o - [ 61%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/upolynomial.cpp.o - [ 62%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/value.cpp.o - [ 62%] Building CXX object src/CMakeFiles/static_pic_polyxx.dir/polyxx/variable.cpp.o - [ 62%] Built target static_poly - [ 63%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/algebraic_number.cpp.o - [ 63%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/assignment.cpp.o - [ 64%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/context.cpp.o - [ 64%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/dyadic_interval.cpp.o - [ 64%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/dyadic_rational.cpp.o - [ 64%] Built target poly - [ 64%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/integer.cpp.o - [ 65%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/integer_ring.cpp.o - [ 66%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/interval_assignment.cpp.o - [ 66%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/interval.cpp.o - [ 67%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/polynomial.cpp.o - [ 67%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/polynomial_utils.cpp.o - [ 68%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/rational.cpp.o - [ 69%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/sign_condition.cpp.o - [ 69%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/rational_interval.cpp.o - [ 69%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/algebraic_number.cpp.o - [ 69%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/dyadic_rational.cpp.o - [ 69%] Building C object python/CMakeFiles/polypy.dir/polypy.c.o - [ 70%] Building C object python/CMakeFiles/polypy.dir/polypyUPolynomial.c.o - [ 71%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/interval_assignment.cpp.o - [ 71%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/integer.cpp.o - [ 72%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/integer_ring.cpp.o - [ 72%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/utils.cpp.o - [ 72%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/context.cpp.o - [ 72%] Building C object python/CMakeFiles/polypy.dir/polypyFeasibilitySet.c.o - [ 73%] Building C object python/CMakeFiles/polypy.dir/polypyVariable.c.o - [ 74%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/rational_interval.cpp.o - [ 72%] Building C object python/CMakeFiles/polypy.dir/polypyInterval.c.o - [ 74%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/rational.cpp.o - [ 75%] Building C object python/CMakeFiles/polypy.dir/polypyAssignment.c.o - [ 75%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/sign_condition.cpp.o - [ 75%] Building C object python/CMakeFiles/polypy.dir/polypyInteger.c.o - [ 75%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/polynomial_utils.cpp.o - [ 76%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/interval.cpp.o - [ 76%] Building C object python/CMakeFiles/polypy.dir/utils.c.o - [ 77%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/value.cpp.o - [ 77%] Building C object python/CMakeFiles/polypy.dir/polypyVariableOrder.c.o - [ 77%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/variable.cpp.o - [ 78%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/upolynomial.cpp.o - [ 79%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/assignment.cpp.o - [ 80%] Building C object python/CMakeFiles/polypy.dir/polypyAlgebraicNumber.c.o - [ 80%] Building CXX object src/CMakeFiles/static_polyxx.dir/polyxx/upolynomial.cpp.o - [ 80%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/dyadic_interval.cpp.o - [ 81%] Building C object python/CMakeFiles/polypy.dir/polypyPolynomial.c.o - [ 82%] Building C object python/CMakeFiles/polypy.dir/polypyValue.c.o - [ 83%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/value.cpp.o - [ 83%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/utils.cpp.o - [ 83%] Building CXX object src/CMakeFiles/polyxx.dir/polyxx/polynomial.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 libpicpolyxx.a - [ 85%] Built target static_pic_polyxx - [ 86%] Linking CXX static library libpolyxx.a - [ 87%] Linking CXX shared library libpolyxx.so - [ 87%] Built target static_polyxx - [ 87%] Built target polyxx - [ 88%] Building CXX object test/poly/CMakeFiles/test_feasible_int_set.dir/test_feasible_int_set.cpp.o - [ 87%] Building CXX object test/polyxx/CMakeFiles/test_dyadic_rational.dir/test_dyadic_rational.cpp.o - [ 88%] Building CXX object test/polyxx/CMakeFiles/test_algebraic_number.dir/test_algebraic_number.cpp.o - [ 88%] Building CXX object test/polyxx/CMakeFiles/test_rational.dir/test_rational.cpp.o - [ 88%] Building CXX object test/polyxx/CMakeFiles/test_dyadic_interval.dir/test_dyadic_interval.cpp.o - [ 89%] Building CXX object test/polyxx/CMakeFiles/test_interval_assignment.dir/test_interval_assignment.cpp.o - [ 89%] Building CXX object test/polyxx/CMakeFiles/test_assignment.dir/test_assignment.cpp.o - [ 90%] Building CXX object test/polyxx/CMakeFiles/test_interval.dir/test_interval.cpp.o - [ 91%] Building CXX object test/polyxx/CMakeFiles/test_integer.dir/test_integer.cpp.o - [ 92%] Building CXX object test/polyxx/CMakeFiles/test_polynomial.dir/test_polynomial.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_upolynomial.dir/test_upolynomial.cpp.o - [ 92%] Building CXX object test/polyxx/CMakeFiles/test_variable.dir/test_variable.cpp.o - [ 92%] Building CXX object test/polyxx/CMakeFiles/test_value.dir/test_value.cpp.o - [ 92%] Linking CXX executable test_interval_assignment - [ 93%] Linking CXX executable test_variable - [ 94%] Linking CXX executable test_assignment - [ 95%] Linking CXX executable test_rational_interval - [ 95%] Built target test_interval_assignment - [ 95%] Linking CXX executable test_polynomial - [ 95%] Built target test_variable - [ 96%] Linking CXX executable test_algebraic_number - [ 96%] Built target test_assignment - [ 96%] Built target test_rational_interval - [ 97%] Linking CXX executable test_dyadic_interval - [ 97%] Built target test_polynomial - [ 97%] Built target test_algebraic_number - [ 98%] Linking CXX executable test_rational - [ 98%] Linking CXX executable test_integer - [ 98%] Built target test_dyadic_interval - [ 98%] Linking CXX executable test_dyadic_rational - [ 98%] Linking CXX executable test_feasible_int_set - [ 98%] Linking CXX executable test_interval - [ 98%] Built target test_rational - [ 98%] Built target test_integer - [ 99%] Linking CXX executable test_upolynomial - [100%] Linking CXX executable test_value - [100%] Built target test_dyadic_rational - [100%] Built target test_interval - [100%] Built target test_feasible_int_set - [100%] Built target test_upolynomial - [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 13.3.0 - -- The CXX compiler identification is GNU 13.3.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.43.0") - 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' - -- Using GNU gold linker. - -- Disabling unit tests since assertions are disabled. - -- Found Python: /usr/bin/python3 (found version "3.12.3") 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 : -fuse-ld=gold - - Install prefix : /usr/local - - cvc5 license: modified BSD - - Note that this configuration is NOT built against any GPL'ed libraries, so - it is covered by the (modified) BSD license. To build against GPL'ed - libraries which can improve cvc5's performance on arithmetic and bit-vector - logics, use the 'configure.sh' script to re-configure with '--best --gpl'. - - Now change to 'build' and type 'make', followed by 'make check' or 'make install'. - - -- Configuring done (15.7s) - -- Generating done (4.4s) - -- 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' - make[1]: Entering directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - make[2]: Entering directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - make[2]: Entering directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - make[2]: Entering directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - make[2]: Entering directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - make[2]: Entering directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - make[2]: Entering directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - make[2]: Entering directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - make[2]: Leaving directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - make[2]: Entering directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - make[2]: Leaving directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - make[2]: Entering directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - make[2]: Entering directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - make[2]: Leaving directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - make[2]: Leaving directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - make[2]: Entering directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - make[2]: Leaving directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - make[2]: Entering directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - make[2]: Entering directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - make[2]: Leaving directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - make[2]: Entering directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - make[2]: Leaving directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - [ 0%] Generating metakind.h - -- Found Git: /usr/bin/git (found version "2.43.0") - [ 0%] Generating theory_traits.h - [ 0%] Generating type_enumerator.cpp - [ 0%] Generating type_checker.cpp - [ 0%] Building CXX object src/context/CMakeFiles/cvc5context.dir/context.cpp.o - [ 0%] Generating options/options.stamp - [ 0%] Generating rewriter_tables.h - [ 0%] Generating kind.h - make[2]: Entering directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - make[2]: Leaving directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - make[2]: Leaving directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - [ 1%] Generating smt2_tokens.h - make[2]: Entering directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - [ 2%] Building CXX object src/context/CMakeFiles/cvc5context.dir/context_mm.cpp.o - [ 2%] Generating node_manager.h - [ 2%] Generating type_properties.h - [ 2%] Generating Trace_tags.h - make[2]: Leaving directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - [ 2%] Built target gen-versioninfo - [ 2%] Generating rewrites.{h,cpp} - [ 2%] Built target gen-tokens - make[2]: Leaving directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - [ 2%] Built target gen-theory - make[2]: Leaving directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - [ 2%] Built target gen-tags - make[2]: Entering directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - make[2]: Leaving directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - make[2]: Entering directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - [ 2%] Building CXX object src/base/CMakeFiles/cvc5base.dir/check.cpp.o - [ 2%] Building CXX object src/base/CMakeFiles/cvc5base.dir/exception.cpp.o - [ 2%] Building CXX object src/base/CMakeFiles/cvc5base.dir/configuration.cpp.o - [ 2%] Building CXX object src/base/CMakeFiles/cvc5base.dir/output.cpp.o - [ 2%] Building CXX object src/base/CMakeFiles/cvc5base.dir/versioninfo.cpp.o - [ 3%] Building CXX object src/base/CMakeFiles/cvc5base.dir/listener.cpp.o - make[2]: Leaving directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - [ 3%] Built target gen-options - [ 3%] Generating kind.cpp - [ 3%] Generating metakind.cpp - [ 3%] Generating node_manager.cpp - [ 3%] Generating type_properties.cpp - make[2]: Leaving directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - [ 3%] Built target gen-expr - make[2]: Entering directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - make[2]: Leaving directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - make[2]: Entering directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - [ 3%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/command_status.cpp.o - [ 3%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/commands.cpp.o - [ 3%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/input.cpp.o - [ 3%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/lexer.cpp.o - [ 4%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/parser.cpp.o - [ 4%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/parse_op.cpp.o - [ 4%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/smt2/smt2_state.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/parser_utils.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_lexer.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/sym_manager.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/tokens.cpp.o - make[2]: Leaving directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - [ 5%] Built target cvc5base - make[2]: Leaving directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - [ 5%] Built target cvc5context - make[2]: Leaving directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - [ 5%] Built target gen-rewrites - make[2]: Entering directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - make[2]: Leaving directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - make[2]: Entering directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - [ 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.cpp.o - [ 7%] Building CXX object src/CMakeFiles/cvc5-obj.dir/api/c/cvc5_c_structs.cpp.o - [ 7%] Building CXX object src/CMakeFiles/cvc5-obj.dir/api/cpp/cvc5_skolem_id.cpp.o - [ 7%] Building CXX object src/CMakeFiles/cvc5-obj.dir/api/cpp/cvc5_types.cpp.o - [ 7%] Building CXX object src/CMakeFiles/cvc5-obj.dir/decision/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/decision_engine.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/managed_streams.cpp.o - [ 8%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/language.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/options_handler.cpp.o - [ 8%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/assertion_pipeline.cpp.o - [ 9%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/learned_literal_manager.cpp.o - [ 9%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/apply_substs.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/bool_to_bv.cpp.o - [ 9%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/bv_eager_atoms.cpp.o - [ 9%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/bv_gauss.cpp.o - [ 9%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/bv_intro_pow2.cpp.o - [ 9%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/bv_to_bool.cpp.o - [ 9%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/bv_to_int.cpp.o - [ 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/global_negate.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/extended_rewriter_pass.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/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/ff_disjunctive_bit.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/ite_simp.cpp.o - [ 10%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/learned_rewrite.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/miplib_trick.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/rewrite.cpp.o - [ 11%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/quantifiers_preprocess.cpp.o - [ 11%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/real_to_int.cpp.o - [ 11%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/sort_infer.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/static_learning.cpp.o - [ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/static_rewrite.cpp.o - [ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/strings_eager_pp.cpp.o - [ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/sygus_inference.cpp.o - [ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/synth_rew_rules.cpp.o - [ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/theory_preprocess.cpp.o - [ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/unconstrained_simplifier.cpp.o - [ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/preprocessing_pass.cpp.o - [ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/preprocessing_pass_context.cpp.o - [ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/preprocessing_pass_registry.cpp.o - [ 14%] Building CXX object src/CMakeFiles/cvc5-obj.dir/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 - [ 14%] 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/eager_proof_generator.cpp.o - [ 15%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/dot/dot_printer.cpp.o - [ 15%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/lazy_proof.cpp.o - [ 15%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/lazy_proof_chain.cpp.o - [ 16%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/lazy_tree_proof_generator.cpp.o - [ 16%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/lfsc/lfsc_list_sc_node_converter.cpp.o - [ 16%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/lfsc/lfsc_node_converter.cpp.o - [ 16%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/lfsc/lfsc_post_processor.cpp.o - [ 16%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/lfsc/lfsc_printer.cpp.o - [ 16%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/lfsc/lfsc_print_channel.cpp.o - [ 16%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/lfsc/lfsc_util.cpp.o - [ 16%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/method_id.cpp.o - [ 16%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/print_expr.cpp.o - [ 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.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_algorithm.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_converter.cpp.o - [ 17%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof_node_to_sexpr.cpp.o - [ 19%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof_node_manager.cpp.o - [ 19%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof_node_updater.cpp.o - [ 19%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof_rule_checker.cpp.o - [ 19%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof_step_buffer.cpp.o - [ 19%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/resolution_proofs_util.cpp.o - [ 19%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/subtype_elim_proof_converter.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/trust_id.cpp.o - [ 19%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/trust_node.cpp.o - [ 19%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/trust_proof_generator.cpp.o - [ 19%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/theory_proof_step_buffer.cpp.o - [ 20%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/unsat_core.cpp.o - [ 20%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/valid_witness_proof_generator.cpp.o - [ 20%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/alethe/alethe_let_binding.cpp.o - [ 20%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/alethe/alethe_node_converter.cpp.o - [ 20%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/alethe/alethe_post_processor.cpp.o - [ 20%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/alethe/alethe_printer.cpp.o - [ 20%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/alethe/alethe_proof_rule.cpp.o - [ 20%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/cadical.cpp.o - [ 20%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/cnf_stream.cpp.o - [ 20%] Building CXX object src/CMakeFiles/cvc5-obj.dir/prop/cryptominisat.cpp.o - [ 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/learned_db.cpp.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/core/Solver.cc.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_proof_manager.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/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/context_manager.cpp.o - [ 23%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/difficulty_post_processor.cpp.o - [ 23%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/env.cpp.o - [ 23%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/env_obj.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/interpolation_solver.cpp.o - [ 25%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/model.cpp.o - [ 25%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/model_core_builder.cpp.o - [ 25%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/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/preprocess_proof_generator.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/process_assertions.cpp.o - [ 25%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/proof_manager.cpp.o - [ 26%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/proof_final_callback.cpp.o - [ 26%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/proof_logger.cpp.o - [ 26%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/proof_post_processor.cpp.o - [ 26%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/proof_post_processor_dsl.cpp.o - [ 26%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/set_defaults.cpp.o - [ 26%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/solver_engine_state.cpp.o - [ 26%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/solver_engine.cpp.o - [ 26%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/solver_engine_stats.cpp.o - [ 26%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/smt_driver.cpp.o - [ 26%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/smt_driver_deep_restarts.cpp.o - [ 27%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/smt_mode.cpp.o - [ 27%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/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/timeout_core_manager.cpp.o - [ 27%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/unsat_core_manager.cpp.o - [ 27%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/arith_evaluator.cpp.o - [ 27%] Building CXX object src/CMakeFiles/cvc5-obj.dir/smt/witness_form.cpp.o - [ 27%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/arith_ite_utils.cpp.o - [ 28%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/arith_msum.cpp.o - [ 28%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/arith_poly_norm.cpp.o - [ 28%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/arith_preprocess.cpp.o - [ 28%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/arith_proof_rcons.cpp.o - [ 28%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/arith_proof_utilities.cpp.o - [ 28%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/arith_rewriter.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/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/arith_utilities.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/arithvar.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/attempt_solution_simplex.cpp.o - [ 29%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/callbacks.cpp.o - [ 29%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/congruence_manager.cpp.o - [ 29%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/constraint.cpp.o - [ 30%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/cut_log.cpp.o - [ 30%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/dio_solver.cpp.o - [ 30%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/dual_simplex.cpp.o - [ 30%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/linear_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_equality.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/matrix.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/normal_form.cpp.o - [ 32%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/partial_model.cpp.o - [ 32%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/simplex.cpp.o - [ 32%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/simplex_update.cpp.o - [ 32%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/tableau.cpp.o - [ 32%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/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/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/projections.cpp.o - [ 33%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/coverings/proof_checker.cpp.o - [ 33%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/coverings/proof_generator.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 - [ 34%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/ext/constraint.cpp.o - [ 34%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/ext/factoring_check.cpp.o - [ 34%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/ext/monomial.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/split_zero_check.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/tangent_plane_check.cpp.o - [ 34%] 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/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/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 - [ 35%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/poly_conversion.cpp.o - [ 36%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/pow2_solver.cpp.o - [ 36%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/stats.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/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/taylor_generator.cpp.o - [ 36%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/operator_elim.cpp.o - [ 36%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/strategy.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/nl/transcendental/exponential_solver.cpp.o - [ 36%] 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/pp_rewrite_eq.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/addition.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/arrays/array_info.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/arith/theory_arith.cpp.o - make[2]: Leaving directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - [ 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[2]: Leaving directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - make[1]: Leaving directory '/home/opam/.opam/default/.opam-switch/build/cvc5.1.3.0-1/_build/default/vendor/cvc5/build' - 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:188: src/parser/CMakeFiles/cvc5parser-objs.dir/smt2/smt2_state.cpp.o] Error 1 - make[2]: *** Waiting for unfinished jobs.... - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/parser/CMakeFiles/cvc5parser-objs.dir/build.make:76: src/parser/CMakeFiles/cvc5parser-objs.dir/commands.cpp.o] Error 1 - make[2]: *** [src/parser/CMakeFiles/cvc5parser-objs.dir/build.make:202: 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:244: src/parser/CMakeFiles/cvc5parser-objs.dir/smt2/smt2_term_parser.cpp.o] Error 1 - make[1]: *** [CMakeFiles/Makefile2:892: 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. - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:76: src/CMakeFiles/cvc5-obj.dir/api/c/cvc5.cpp.o] Error 1 - make[2]: *** Waiting for unfinished jobs.... - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:524: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/foreign_theory_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:426: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/bv_gauss.cpp.o] Error 1 - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:454: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/bv_to_bool.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:104: src/CMakeFiles/cvc5-obj.dir/api/cpp/cvc5.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:188: src/CMakeFiles/cvc5-obj.dir/decision/justify_cache.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:342: 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:90: 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. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:202: src/CMakeFiles/cvc5-obj.dir/decision/justify_info.cpp.o] Error 1 - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:622: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/learned_rewrite.cpp.o] Error 1 - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:468: 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:398: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/bool_to_bv.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:160: 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:174: src/CMakeFiles/cvc5-obj.dir/decision/justification_strategy.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:412: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/bv_eager_atoms.cpp.o] Error 1 - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:580: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/int_to_bv.cpp.o] Error 1 - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:664: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/non_clausal_simp.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:566: 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:608: 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:510: 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:146: src/CMakeFiles/cvc5-obj.dir/decision/assertion_list.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:482: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/extended_rewriter_pass.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:846: 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:1210: src/CMakeFiles/cvc5-obj.dir/proof/lfsc/lfsc_node_converter.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:860: 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:636: 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:370: 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:356: src/CMakeFiles/cvc5-obj.dir/preprocessing/learned_literal_manager.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:804: 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:384: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/apply_substs.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:776: 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:916: 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:1546: src/CMakeFiles/cvc5-obj.dir/proof/trust_node.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1070: src/CMakeFiles/cvc5-obj.dir/proof/assumption_proof_generator.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:748: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/sort_infer.cpp.o] Error 1 - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1266: 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:594: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/ite_removal.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1028: src/CMakeFiles/cvc5-obj.dir/proof/alf/alf_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. - 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. - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:496: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/ff_bitsum.cpp.o] Error 1 - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:650: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/nl_ext_purify.cpp.o] Error 1 - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1112: src/CMakeFiles/cvc5-obj.dir/proof/conv_seq_proof_generator.cpp.o] Error 1 - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1168: src/CMakeFiles/cvc5-obj.dir/proof/lazy_proof_chain.cpp.o] Error 1 - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1224: src/CMakeFiles/cvc5-obj.dir/proof/lfsc/lfsc_post_processor.cpp.o] Error 1 - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1378: src/CMakeFiles/cvc5-obj.dir/proof/proof_node.cpp.o] Error 1 - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1420: src/CMakeFiles/cvc5-obj.dir/proof/proof_node_to_sexpr.cpp.o] Error 1 - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2666: src/CMakeFiles/cvc5-obj.dir/theory/arith/branch_and_bound.cpp.o] Error 1 - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2736: src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/arith_static_learner.cpp.o] Error 1 - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:3408: src/CMakeFiles/cvc5-obj.dir/theory/arith/nl/icp/icp_solver.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2218: 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:2988: src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/simplex_update.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:720: 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:930: 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:2946: src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/normal_form.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1140: 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:1588: 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:706: 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:1280: 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:1798: src/CMakeFiles/cvc5-obj.dir/prop/minisat/opt_clauses_manager.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:888: src/CMakeFiles/cvc5-obj.dir/preprocessing/preprocessing_pass_registry.cpp.o] Error 1 - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1154: src/CMakeFiles/cvc5-obj.dir/proof/lazy_proof.cpp.o] Error 1 - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2106: src/CMakeFiles/cvc5-obj.dir/smt/listeners.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2036: 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:1126: 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:1448: 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:552: 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:1644: 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:1392: src/CMakeFiles/cvc5-obj.dir/proof/proof_node_algorithm.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:986: 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:692: 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:538: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/fun_def_fmf.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1406: 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:1238: src/CMakeFiles/cvc5-obj.dir/proof/lfsc/lfsc_printer.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1084: 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:1042: 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:1532: src/CMakeFiles/cvc5-obj.dir/proof/trust_id.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:2050: src/CMakeFiles/cvc5-obj.dir/smt/env.cpp.o] Error 1 - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:958: 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:1658: src/CMakeFiles/cvc5-obj.dir/proof/alethe/alethe_printer.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:818: 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:1000: 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:2288: 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:2358: 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:1574: src/CMakeFiles/cvc5-obj.dir/proof/theory_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:1322: 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:1686: 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:2470: src/CMakeFiles/cvc5-obj.dir/smt/timeout_core_manager.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:440: 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:832: 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:1056: 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:1504: 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:1756: src/CMakeFiles/cvc5-obj.dir/prop/lemma_inprocess.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:1350: src/CMakeFiles/cvc5-obj.dir/proof/proof_generator.cpp.o] Error 1 - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1980: 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:1868: src/CMakeFiles/cvc5-obj.dir/prop/prop_engine.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1462: src/CMakeFiles/cvc5-obj.dir/proof/proof_rule_checker.cpp.o] Error 1 - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2316: 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:972: src/CMakeFiles/cvc5-obj.dir/printer/printer.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1826: 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:2092: 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:734: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/sep_skolem_emp.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2778: src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/callbacks.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1882: 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:2330: src/CMakeFiles/cvc5-obj.dir/smt/set_defaults.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:678: 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:2232: src/CMakeFiles/cvc5-obj.dir/smt/print_benchmark.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:874: src/CMakeFiles/cvc5-obj.dir/preprocessing/preprocessing_pass_context.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:790: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/strings_eager_pp.cpp.o] Error 1 - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2596: src/CMakeFiles/cvc5-obj.dir/theory/arith/arith_proof_utilities.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1770: 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:762: src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/static_learning.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1630: 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:2134: 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:2176: 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:1602: 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:2610: src/CMakeFiles/cvc5-obj.dir/theory/arith/arith_rewriter.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2890: src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/infer_bounds.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2274: 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:2498: src/CMakeFiles/cvc5-obj.dir/smt/witness_form.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2820: 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:2064: 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:2918: 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:2862: src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/error_set.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2190: 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:2764: src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/attempt_solution_simplex.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2456: src/CMakeFiles/cvc5-obj.dir/smt/term_formula_removal.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:3044: src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/theory_arith_private.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2022: src/CMakeFiles/cvc5-obj.dir/smt/context_manager.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1182: 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:2806: src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/constraint.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:2512: 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:1966: src/CMakeFiles/cvc5-obj.dir/prop/zero_level_learner.cpp.o] Error 1 - c++: fatal error: Killed signal terminated program cc1plus - compilation terminated. - make[2]: *** [src/CMakeFiles/cvc5-obj.dir/build.make:1784: 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:1700: 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:1840: 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:1896: 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:2708: 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:1938: 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:1952: 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:2246: 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:2302: src/CMakeFiles/cvc5-obj.dir/smt/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:2008: 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:2904: src/CMakeFiles/cvc5-obj.dir/theory/arith/linear/linear_solver.cpp.o] Error 1 - make[1]: *** [CMakeFiles/Makefile2:732: 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...