Reading package lists... Building dependency tree... Reading state information... Need to get 1,188 kB of source archives. Get:1 http://urika:3142/ftp.debian.org/debian/ sid/main cvc3 2.4.1-5 (dsc) [2,081 B] Get:2 http://urika:3142/ftp.debian.org/debian/ sid/main cvc3 2.4.1-5 (tar) [1,176 kB] Get:3 http://urika:3142/ftp.debian.org/debian/ sid/main cvc3 2.4.1-5 (diff) [10.1 kB] gpgv: keyblock resource `/tmp/.gnupg/trustedkeys.gpg': file open error gpgv: Signature made Sat 27 Sep 2014 08:04:50 PM UTC using RSA key ID E3386741 gpgv: Can't check signature: public key not found dpkg-source: warning: failed to verify signature on ./cvc3_2.4.1-5.dsc dpkg-source: info: extracting cvc3 in cvc3-2.4.1 dpkg-source: info: unpacking cvc3_2.4.1.orig.tar.gz tar: A lone zero block at 11280 dpkg-source: info: unpacking cvc3_2.4.1-5.debian.tar.xz dpkg-source: info: applying disable-log-dumps-in-tests.patch Fetched 1,188 kB in 0s (1,287 kB/s) Reading package lists... Building dependency tree... Reading state information... The following NEW packages will be installed: bison flex libbison-dev libfl-dev libgmp-dev libgmpxx4ldbl patchutils 0 upgraded, 7 newly installed, 0 to remove and 1 not upgraded. Need to get 2,420 kB of archives. After this operation, 6,404 kB of additional disk space will be used. Get:1 http://urika:3142/ftp.debian.org/debian/ sid/main libfl-dev amd64 2.5.39-8+b1 [75.4 kB] Get:2 http://urika:3142/ftp.debian.org/debian/ sid/main flex amd64 2.5.39-8+b1 [422 kB] Get:3 http://urika:3142/ftp.debian.org/debian/ sid/main libbison-dev amd64 2:3.0.2.dfsg-2 [426 kB] Get:4 http://urika:3142/ftp.debian.org/debian/ sid/main bison amd64 2:3.0.2.dfsg-2 [765 kB] Get:5 http://urika:3142/ftp.debian.org/debian/ sid/main libgmpxx4ldbl amd64 2:6.0.0+dfsg-7 [22.2 kB] Get:6 http://urika:3142/ftp.debian.org/debian/ sid/main libgmp-dev amd64 2:6.0.0+dfsg-7 [621 kB] Get:7 http://urika:3142/ftp.debian.org/debian/ sid/main patchutils amd64 0.3.4-1 [89.1 kB] debconf: delaying package configuration, since apt-utils is not installed Fetched 2,420 kB in 0s (25.5 MB/s) Selecting previously unselected package libfl-dev:amd64. (Reading database ... (Reading database ... 5% (Reading database ... 10% (Reading database ... 15% (Reading database ... 20% (Reading database ... 25% (Reading database ... 30% (Reading database ... 35% (Reading database ... 40% (Reading database ... 45% (Reading database ... 50% (Reading database ... 55% (Reading database ... 60% (Reading database ... 65% (Reading database ... 70% (Reading database ... 75% (Reading database ... 80% (Reading database ... 85% (Reading database ... 90% (Reading database ... 95% (Reading database ... 100% (Reading database ... 82591 files and directories currently installed.) Preparing to unpack .../libfl-dev_2.5.39-8+b1_amd64.deb ... Unpacking libfl-dev:amd64 (2.5.39-8+b1) ... Selecting previously unselected package flex. Preparing to unpack .../flex_2.5.39-8+b1_amd64.deb ... Unpacking flex (2.5.39-8+b1) ... Selecting previously unselected package libbison-dev:amd64. Preparing to unpack .../libbison-dev_2%3a3.0.2.dfsg-2_amd64.deb ... Unpacking libbison-dev:amd64 (2:3.0.2.dfsg-2) ... Selecting previously unselected package bison. Preparing to unpack .../bison_2%3a3.0.2.dfsg-2_amd64.deb ... Unpacking bison (2:3.0.2.dfsg-2) ... Selecting previously unselected package libgmpxx4ldbl:amd64. Preparing to unpack .../libgmpxx4ldbl_2%3a6.0.0+dfsg-7_amd64.deb ... Unpacking libgmpxx4ldbl:amd64 (2:6.0.0+dfsg-7) ... Selecting previously unselected package libgmp-dev:amd64. Preparing to unpack .../libgmp-dev_2%3a6.0.0+dfsg-7_amd64.deb ... Unpacking libgmp-dev:amd64 (2:6.0.0+dfsg-7) ... Selecting previously unselected package patchutils. Preparing to unpack .../patchutils_0.3.4-1_amd64.deb ... Unpacking patchutils (0.3.4-1) ... Processing triggers for man-db (2.7.2-1) ... Setting up libfl-dev:amd64 (2.5.39-8+b1) ... Setting up flex (2.5.39-8+b1) ... Setting up libbison-dev:amd64 (2:3.0.2.dfsg-2) ... Setting up bison (2:3.0.2.dfsg-2) ... update-alternatives: using /usr/bin/bison.yacc to provide /usr/bin/yacc (yacc) in auto mode Setting up libgmpxx4ldbl:amd64 (2:6.0.0+dfsg-7) ... Setting up libgmp-dev:amd64 (2:6.0.0+dfsg-7) ... Setting up patchutils (0.3.4-1) ... Processing triggers for libc-bin (2.19-19) ... Killed old client process Internet Systems Consortium DHCP Client 4.3.2 Copyright 2004-2015 Internet Systems Consortium. All rights reserved. For info, please visit https://www.isc.org/software/dhcp/ Listening on LPF/eth0/2a:f3:b0:8b:25:6c Sending on LPF/eth0/2a:f3:b0:8b:25:6c Sending on Socket/fallback DHCPRELEASE on eth0 to 10.0.3.1 port 67 dpkg-buildpackage: source package cvc3 dpkg-buildpackage: source version 2.4.1-5 dpkg-buildpackage: source distribution unstable dpkg-buildpackage: source changed by Morgan Deters dpkg-source --before-build cvc3-2.4.1 dpkg-buildpackage: host architecture amd64 debian/rules clean test -x debian/rules rm -f java/Test_manifest dh_autotools-dev_updateconfig ./configure --disable-zchaff checking for g++... g++ checking whether the C++ compiler works... yes checking for C++ compiler default output file name... a.out checking for suffix of executables... checking whether we are cross compiling... no checking for suffix of object files... o checking whether we are using the GNU C++ compiler... yes checking whether g++ accepts -g... yes checking how to run the C++ preprocessor... g++ -E checking for ar... ar checking build system type... x86_64-unknown-linux-gnu checking host system type... x86_64-unknown-linux-gnu checking for install... /usr/bin/install checking for ldconfig... /sbin/ldconfig checking for time... not found configure: WARNING: Regression tests depend upon GNU time. checking for perl... /usr/bin/perl checking for bison... bison -y checking for flex... flex checking lex output file root... lex.yy checking lex library... none needed checking whether yytext is a pointer... no checking for compiler version (g++ --version)... 5.2.1 checking for gmp... yes checking vector usability... yes checking vector presence... yes checking for vector... yes checking list usability... yes checking list presence... yes checking for list... yes checking deque usability... yes checking deque presence... yes checking for deque... yes checking set usability... yes checking set presence... yes checking for set... yes checking string usability... yes checking string presence... yes checking for string... yes checking cstdlib usability... yes checking cstdlib presence... yes checking for cstdlib... yes checking cstdio usability... yes checking cstdio presence... yes checking for cstdio... yes checking functional usability... yes checking functional presence... yes checking for functional... yes checking algorithm usability... yes checking algorithm presence... yes checking for algorithm... yes checking for doxygen... no checking for doxytag... no checking for fig2dev... no checking for dot... NO checking for etags... no checking for ebrowse... no configure: creating ./config.status config.status: creating Makefile.local config.status: creating LICENSE config.status: creating src/cvc3.pc config.status: creating bin/unpack config.status: creating bin/run_tests config.status: creating bin/cvc2smt config.status: creating doc/Doxyfile config.status: creating doc/Makefile CVC3 is configured successfully. Platform: x86_64-linux-gnu Version: 2.4.1 Computer arithmetic: GMP Run ./configure --help for additional configuration options. Type 'make' to compile CVC3. dh_autotools-dev_restoreconfig rm -f debian/stamp-makefile-build debian/stamp-makefile-install /usr/bin/make -C . -k distclean TOP=/cvc3-2.4.1 make[1]: Entering directory '/cvc3-2.4.1' cd /cvc3-2.4.1/src; /usr/bin/make distclean make[2]: Entering directory '/cvc3-2.4.1/src' /usr/bin/make build TARGET=distclean make[3]: Entering directory '/cvc3-2.4.1/src' cd util && /usr/bin/make distclean make[4]: Entering directory '/cvc3-2.4.1/src/util' Making dependencies for debug.cpp statistics.cpp rational.cpp rational-native.cpp rational-gmp.cpp g++ -M -m64 -O2 -Wall -I. -I/cvc3-2.4.1/src/include -DRATIONAL_GMP debug.cpp statistics.cpp rational.cpp rational-native.cpp rational-gmp.cpp >> /cvc3-2.4.1/obj/util/x86_64-linux-gnu/Makefile.tmp rm -f make[4]: Leaving directory '/cvc3-2.4.1/src/util' cd context && /usr/bin/make distclean make[4]: Entering directory '/cvc3-2.4.1/src/context' Making dependencies for context.cpp cdflags.cpp g++ -M -m64 -O2 -Wall -I. -I/cvc3-2.4.1/src/include context.cpp cdflags.cpp >> /cvc3-2.4.1/obj/context/x86_64-linux-gnu/Makefile.tmp rm -f make[4]: Leaving directory '/cvc3-2.4.1/src/context' cd expr && /usr/bin/make distclean make[4]: Entering directory '/cvc3-2.4.1/src/expr' Making dependencies for expr.cpp expr_manager.cpp expr_stream.cpp expr_value.cpp expr_op.cpp g++ -M -m64 -O2 -Wall -I. -I/cvc3-2.4.1/src/include expr.cpp expr_manager.cpp expr_stream.cpp expr_value.cpp expr_op.cpp >> /cvc3-2.4.1/obj/expr/x86_64-linux-gnu/Makefile.tmp rm -f make[4]: Leaving directory '/cvc3-2.4.1/src/expr' cd theorem && /usr/bin/make distclean make[4]: Entering directory '/cvc3-2.4.1/src/theorem' Making dependencies for assumptions.cpp theorem.cpp theorem_manager.cpp theorem_producer.cpp common_theorem_producer.cpp g++ -M -m64 -O2 -Wall -I. -I/cvc3-2.4.1/src/include assumptions.cpp theorem.cpp theorem_manager.cpp theorem_producer.cpp common_theorem_producer.cpp >> /cvc3-2.4.1/obj/theorem/x86_64-linux-gnu/Makefile.tmp rm -f make[4]: Leaving directory '/cvc3-2.4.1/src/theorem' cd sat && /usr/bin/make distclean make[4]: Entering directory '/cvc3-2.4.1/src/sat' Making dependencies for cnf.cpp cnf_manager.cpp cnf_theorem_producer.cpp dpllt_basic.cpp sat_api.cpp dpllt_minisat.cpp minisat_types.cpp minisat_derivation.cpp minisat_solver.cpp g++ -M -m64 -O2 -Wall -I. -I/cvc3-2.4.1/src/include cnf.cpp cnf_manager.cpp cnf_theorem_producer.cpp dpllt_basic.cpp sat_api.cpp dpllt_minisat.cpp minisat_types.cpp minisat_derivation.cpp minisat_solver.cpp >> /cvc3-2.4.1/obj/sat/x86_64-linux-gnu/Makefile.tmp rm -f make[4]: Leaving directory '/cvc3-2.4.1/src/sat' cd theory_core && /usr/bin/make distclean make[4]: Entering directory '/cvc3-2.4.1/src/theory_core' Making dependencies for theory.cpp theory_core.cpp core_theorem_producer.cpp expr_transform.cpp bryant.cpp g++ -M -m64 -O2 -Wall -I. -I/cvc3-2.4.1/src/include theory.cpp theory_core.cpp core_theorem_producer.cpp expr_transform.cpp bryant.cpp >> /cvc3-2.4.1/obj/theory_core/x86_64-linux-gnu/Makefile.tmp rm -f make[4]: Leaving directory '/cvc3-2.4.1/src/theory_core' cd theory_arith && /usr/bin/make distclean make[4]: Entering directory '/cvc3-2.4.1/src/theory_arith' Making dependencies for arith_theorem_producer_old.cpp arith_theorem_producer.cpp arith_theorem_producer3.cpp theory_arith.cpp theory_arith_old.cpp theory_arith_new.cpp theory_arith3.cpp g++ -M -m64 -O2 -Wall -I. -I/cvc3-2.4.1/src/include arith_theorem_producer_old.cpp arith_theorem_producer.cpp arith_theorem_producer3.cpp theory_arith.cpp theory_arith_old.cpp theory_arith_new.cpp theory_arith3.cpp >> /cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/Makefile.tmp rm -f make[4]: Leaving directory '/cvc3-2.4.1/src/theory_arith' cd theory_array && /usr/bin/make distclean make[4]: Entering directory '/cvc3-2.4.1/src/theory_array' Making dependencies for array_theorem_producer.cpp theory_array.cpp g++ -M -m64 -O2 -Wall -I. -I/cvc3-2.4.1/src/include array_theorem_producer.cpp theory_array.cpp >> /cvc3-2.4.1/obj/theory_array/x86_64-linux-gnu/Makefile.tmp rm -f make[4]: Leaving directory '/cvc3-2.4.1/src/theory_array' cd theory_bitvector && /usr/bin/make distclean make[4]: Entering directory '/cvc3-2.4.1/src/theory_bitvector' Making dependencies for bitvector_theorem_producer.cpp theory_bitvector.cpp g++ -M -m64 -O2 -Wall -I. -I/cvc3-2.4.1/src/include bitvector_theorem_producer.cpp theory_bitvector.cpp >> /cvc3-2.4.1/obj/theory_bitvector/x86_64-linux-gnu/Makefile.tmp rm -f make[4]: Leaving directory '/cvc3-2.4.1/src/theory_bitvector' cd theory_datatype && /usr/bin/make distclean make[4]: Entering directory '/cvc3-2.4.1/src/theory_datatype' Making dependencies for datatype_theorem_producer.cpp theory_datatype.cpp theory_datatype_lazy.cpp g++ -M -m64 -O2 -Wall -I. -I/cvc3-2.4.1/src/include datatype_theorem_producer.cpp theory_datatype.cpp theory_datatype_lazy.cpp >> /cvc3-2.4.1/obj/theory_datatype/x86_64-linux-gnu/Makefile.tmp rm -f make[4]: Leaving directory '/cvc3-2.4.1/src/theory_datatype' cd theory_quant && /usr/bin/make distclean make[4]: Entering directory '/cvc3-2.4.1/src/theory_quant' Making dependencies for theory_quant.cpp quant_theorem_producer.cpp g++ -M -m64 -O2 -Wall -I. -I/cvc3-2.4.1/src/include theory_quant.cpp quant_theorem_producer.cpp >> /cvc3-2.4.1/obj/theory_quant/x86_64-linux-gnu/Makefile.tmp rm -f make[4]: Leaving directory '/cvc3-2.4.1/src/theory_quant' cd theory_records && /usr/bin/make distclean make[4]: Entering directory '/cvc3-2.4.1/src/theory_records' Making dependencies for theory_records.cpp records_theorem_producer.cpp g++ -M -m64 -O2 -Wall -I. -I/cvc3-2.4.1/src/include theory_records.cpp records_theorem_producer.cpp >> /cvc3-2.4.1/obj/theory_records/x86_64-linux-gnu/Makefile.tmp rm -f make[4]: Leaving directory '/cvc3-2.4.1/src/theory_records' cd theory_simulate && /usr/bin/make distclean make[4]: Entering directory '/cvc3-2.4.1/src/theory_simulate' Making dependencies for theory_simulate.cpp simulate_theorem_producer.cpp g++ -M -m64 -O2 -Wall -I. -I/cvc3-2.4.1/src/include theory_simulate.cpp simulate_theorem_producer.cpp >> /cvc3-2.4.1/obj/theory_simulate/x86_64-linux-gnu/Makefile.tmp rm -f make[4]: Leaving directory '/cvc3-2.4.1/src/theory_simulate' cd theory_uf && /usr/bin/make distclean make[4]: Entering directory '/cvc3-2.4.1/src/theory_uf' Making dependencies for uf_theorem_producer.cpp theory_uf.cpp g++ -M -m64 -O2 -Wall -I. -I/cvc3-2.4.1/src/include uf_theorem_producer.cpp theory_uf.cpp >> /cvc3-2.4.1/obj/theory_uf/x86_64-linux-gnu/Makefile.tmp rm -f make[4]: Leaving directory '/cvc3-2.4.1/src/theory_uf' cd search && /usr/bin/make distclean make[4]: Entering directory '/cvc3-2.4.1/src/search' Making dependencies for clause.cpp search_impl_base.cpp search.cpp search_fast.cpp search_theorem_producer.cpp search_sat.cpp search_simple.cpp variable.cpp circuit.cpp decision_engine.cpp decision_engine_dfs.cpp LFSCObject.cpp LFSCUtilProof.cpp LFSCBoolProof.cpp LFSCConvert.cpp LFSCLraProof.cpp LFSCPrinter.cpp LFSCProof.cpp TReturn.cpp Util.cpp g++ -M -m64 -O2 -Wall -I. -I/cvc3-2.4.1/src/include clause.cpp search_impl_base.cpp search.cpp search_fast.cpp search_theorem_producer.cpp search_sat.cpp search_simple.cpp variable.cpp circuit.cpp decision_engine.cpp decision_engine_dfs.cpp LFSCObject.cpp LFSCUtilProof.cpp LFSCBoolProof.cpp LFSCConvert.cpp LFSCLraProof.cpp LFSCPrinter.cpp LFSCProof.cpp TReturn.cpp Util.cpp >> /cvc3-2.4.1/obj/search/x86_64-linux-gnu/Makefile.tmp rm -f make[4]: Leaving directory '/cvc3-2.4.1/src/search' cd parser && /usr/bin/make distclean make[4]: Entering directory '/cvc3-2.4.1/src/parser' bison -d -y -o parsePL.cpp -p PL --debug -v PL.y PL.y: warning: 3 shift/reduce conflicts [-Wconflicts-sr] PL.y:1531.24-1536.25: warning: rule useless in parser due to conflicts [-Wother] AndExpr : AndExpr AND_TOK Expr ^^^^^^^^^^^^^ PL.y:1549.25-1554.25: warning: rule useless in parser due to conflicts [-Wother] OrExpr : OrExpr OR_TOK Expr ^^^^^^^^^^ flex -I -PPL -olexPL.cpp PL.lex bison -d -y -o parseLisp.cpp -p Lisp --debug -v Lisp.y flex -I -PLisp -olexLisp.cpp Lisp.lex bison -d -y -o parsesmtlib.cpp -p smtlib --debug -v smtlib.y flex -I -Psmtlib -olexsmtlib.cpp smtlib.lex bison -d -y -o parsesmtlib2.cpp -p smtlib2 --debug -v smtlib2.y smtlib2.y: warning: 4 shift/reduce conflicts [-Wconflicts-sr] flex -I -Psmtlib2 -olexsmtlib2.cpp smtlib2.lex Making dependencies for parsePL.cpp lexPL.cpp parseLisp.cpp lexLisp.cpp parsesmtlib.cpp lexsmtlib.cpp parsesmtlib2.cpp lexsmtlib2.cpp parser.cpp g++ -M -m64 -O2 -Wall -I. -I/cvc3-2.4.1/src/include -O0 parsePL.cpp lexPL.cpp parseLisp.cpp lexLisp.cpp parsesmtlib.cpp lexsmtlib.cpp parsesmtlib2.cpp lexsmtlib2.cpp parser.cpp >> /cvc3-2.4.1/obj/parser/x86_64-linux-gnu/Makefile.tmp rm -f parsePL.cpp lexPL.cpp parseLisp.cpp lexLisp.cpp parsesmtlib.cpp lexsmtlib.cpp parsesmtlib2.cpp lexsmtlib2.cpp parsePL_defs.h parsePL.output parseLisp_defs.h parseLisp.output parsesmtlib_defs.h parsesmtlib.output parsesmtlib2_defs.h parsesmtlib2.output make[4]: Leaving directory '/cvc3-2.4.1/src/parser' cd translator && /usr/bin/make distclean make[4]: Entering directory '/cvc3-2.4.1/src/translator' Making dependencies for translator.cpp g++ -M -m64 -O2 -Wall -I. -I/cvc3-2.4.1/src/include translator.cpp >> /cvc3-2.4.1/obj/translator/x86_64-linux-gnu/Makefile.tmp rm -f make[4]: Leaving directory '/cvc3-2.4.1/src/translator' cd vcl && /usr/bin/make distclean make[4]: Entering directory '/cvc3-2.4.1/src/vcl' Making dependencies for vcl.cpp vc_cmd.cpp g++ -M -m64 -O2 -Wall -I. -I/cvc3-2.4.1/src/include vcl.cpp vc_cmd.cpp >> /cvc3-2.4.1/obj/vcl/x86_64-linux-gnu/Makefile.tmp rm -f make[4]: Leaving directory '/cvc3-2.4.1/src/vcl' cd c_interface && /usr/bin/make distclean make[4]: Entering directory '/cvc3-2.4.1/src/c_interface' Making dependencies for c_interface.cpp g++ -M -m64 -O2 -Wall -I. -I/cvc3-2.4.1/src/include c_interface.cpp >> /cvc3-2.4.1/obj/c_interface/x86_64-linux-gnu/Makefile.tmp rm -f make[4]: Leaving directory '/cvc3-2.4.1/src/c_interface' cd cvc3 && /usr/bin/make distclean VERSION=2.4.1 make[4]: Entering directory '/cvc3-2.4.1/src/cvc3' Making dependencies for main.cpp g++ -M -m64 -O2 -Wall -I. -I/cvc3-2.4.1/src/include -DVERSION=\"2.4.1\" main.cpp >> /cvc3-2.4.1/obj/cvc3/x86_64-linux-gnu/Makefile.tmp rm -f make[4]: Leaving directory '/cvc3-2.4.1/src/cvc3' make[3]: Leaving directory '/cvc3-2.4.1/src' rm -rf cvc3.pc make[2]: Leaving directory '/cvc3-2.4.1/src' cd /cvc3-2.4.1/doc; /usr/bin/make distclean make[2]: Entering directory '/cvc3-2.4.1/doc' make[2]: Leaving directory '/cvc3-2.4.1/doc' cd /cvc3-2.4.1/test; /usr/bin/make distclean make[2]: Entering directory '/cvc3-2.4.1/test' Making dependencies for main.cpp george.cpp g++ -M -m64 -O2 -Wall -I. -I/cvc3-2.4.1/src/include -O0 main.cpp george.cpp >> /cvc3-2.4.1/test/obj/x86_64-linux-gnu/Makefile.tmp rm -f make[2]: Leaving directory '/cvc3-2.4.1/test' cd /cvc3-2.4.1/java; /usr/bin/make distclean make[2]: Entering directory '/cvc3-2.4.1/java' if [ ! -d obj ]; then mkdir -p obj; fi rm -f src/cvc3/EmbeddedManager.cpp src/cvc3/Expr.cpp src/cvc3/ExprMut.cpp src/cvc3/ExprManager.cpp src/cvc3/Type.cpp src/cvc3/TypeMut.cpp src/cvc3/Op.cpp src/cvc3/OpMut.cpp src/cvc3/Rational.cpp src/cvc3/RationalMut.cpp src/cvc3/Theorem.cpp src/cvc3/TheoremMut.cpp src/cvc3/Proof.cpp src/cvc3/ProofMut.cpp src/cvc3/Context.cpp src/cvc3/ContextMut.cpp src/cvc3/Flag.cpp src/cvc3/Flags.cpp src/cvc3/FlagsMut.cpp src/cvc3/Statistics.cpp src/cvc3/StatisticsMut.cpp src/cvc3/ValidityChecker.cpp rm -fr obj/cvc3/* rm -fr /cvc3-2.4.1/java/lib/* rm -f include/cvc3/EmbeddedManager.h include/cvc3/Expr.h include/cvc3/ExprMut.h include/cvc3/ExprManager.h include/cvc3/Type.h include/cvc3/TypeMut.h include/cvc3/Op.h include/cvc3/OpMut.h include/cvc3/Rational.h include/cvc3/RationalMut.h include/cvc3/Theorem.h include/cvc3/TheoremMut.h include/cvc3/Proof.h include/cvc3/ProofMut.h include/cvc3/Context.h include/cvc3/ContextMut.h include/cvc3/Flag.h include/cvc3/Flags.h include/cvc3/FlagsMut.h include/cvc3/Statistics.h include/cvc3/StatisticsMut.h include/cvc3/ValidityChecker.h include/cvc3/EmbeddedManager.h.gch include/cvc3/Expr.h.gch include/cvc3/ExprMut.h.gch include/cvc3/ExprManager.h.gch include/cvc3/Type.h.gch include/cvc3/TypeMut.h.gch include/cvc3/Op.h.gch include/cvc3/OpMut.h.gch include/cvc3/Rational.h.gch include/cvc3/RationalMut.h.gch include/cvc3/Theorem.h.gch include/cvc3/TheoremMut.h.gch include/cvc3/Proof.h.gch include/cvc3/ProofMut.h.gch include/cvc3/Context.h.gch include/cvc3/ContextMut.h.gch include/cvc3/Flag.h.gch include/cvc3/Flags.h.gch include/cvc3/FlagsMut.h.gch include/cvc3/Statistics.h.gch include/cvc3/StatisticsMut.h.gch include/cvc3/ValidityChecker.h.gch include/cvc3/JniUtils.h.gch make[2]: Leaving directory '/cvc3-2.4.1/java' rm -rf /cvc3-2.4.1/test/bin /cvc3-2.4.1/test/obj cd /cvc3-2.4.1/testc; /usr/bin/make distclean make[2]: Entering directory '/cvc3-2.4.1/testc' Making dependencies for gcc -M -g -I../src/include main.c >> /cvc3-2.4.1/testc/obj/x86_64-linux-gnu/Makefile.tmp rm -f /cvc3-2.4.1/testc/obj/x86_64-linux-gnu/main.o make[2]: Leaving directory '/cvc3-2.4.1/testc' rm -rf /cvc3-2.4.1/testc/bin /cvc3-2.4.1/testc/obj mv: cannot stat ‘/cvc3-2.4.1/bin/CVS’: No such file or directory Makefile:153: recipe for target 'distclean' failed make[1]: [distclean] Error 1 (ignored) mv: cannot stat ‘/cvc3-2.4.1/bin/.cvsignore’: No such file or directory Makefile:153: recipe for target 'distclean' failed make[1]: [distclean] Error 1 (ignored) rm -rf /cvc3-2.4.1/bin rm -f TAGS BROWSE FILES LICENSE Makefile.local rm -rf /cvc3-2.4.1/autom4te.cache rm -f config.log config.status rm -f regressions.log rm -rf /cvc3-2.4.1/lib /cvc3-2.4.1/obj make[1]: Leaving directory '/cvc3-2.4.1' rm -f debian/stamp-makefile-check rm -f debian/stamp-autotools rmdir --ignore-fail-on-non-empty . rmdir: failed to remove ‘.’: Invalid argument /usr/share/cdbs/1/class/autotools.mk:52: recipe for target 'makefile-clean' failed make: [makefile-clean] Error 1 (ignored) for i in ./config.guess ./config.sub ; do \ if test -e $i.cdbs-orig ; then \ mv $i.cdbs-orig $i ; \ fi ; \ done dh_clean rm -f debian/stamp-autotools-files dpkg-source -b cvc3-2.4.1 dpkg-source: info: using source format '3.0 (quilt)' dpkg-source: info: building cvc3 using existing ./cvc3_2.4.1.orig.tar.gz tar: A lone zero block at 11280 dpkg-source: warning: ignoring deletion of file java/Test_manifest, use --include-removal to override dpkg-source: info: building cvc3 in cvc3_2.4.1-5.debian.tar.xz dpkg-source: info: building cvc3 in cvc3_2.4.1-5.dsc debian/rules build test -x debian/rules mkdir -p "." if test -e /usr/share/misc/config.guess ; then \ for i in ./config.guess ; do \ if ! test -e $i.cdbs-orig ; then \ mv $i $i.cdbs-orig ; \ cp --remove-destination /usr/share/misc/config.guess $i ; \ fi ; \ done ; \ fi if test -e /usr/share/misc/config.sub ; then \ for i in ./config.sub ; do \ if ! test -e $i.cdbs-orig ; then \ mv $i $i.cdbs-orig ; \ cp --remove-destination /usr/share/misc/config.sub $i ; \ fi ; \ done ; \ fi touch debian/stamp-autotools-files chmod a+x /cvc3-2.4.1/./configure mkdir -p . cd . && CFLAGS="-g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall" CXXFLAGS="-g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall" CPPFLAGS="-D_FORTIFY_SOURCE=2" LDFLAGS="-Wl,-z,relro" /cvc3-2.4.1/./configure --build=x86_64-linux-gnu --prefix=/usr --includedir="\${prefix}/include" --mandir="\${prefix}/share/man" --infodir="\${prefix}/share/info" --sysconfdir=/etc --localstatedir=/var --libexecdir="\${prefix}/lib/cvc3" --srcdir=. --disable-maintainer-mode --disable-dependency-tracking --disable-silent-rules --enable-dynamic --enable-java --with-java-home=/usr/lib/jvm/default-java --disable-zchaff configure: WARNING: unrecognized options: --disable-maintainer-mode, --disable-dependency-tracking, --disable-silent-rules checking for g++... g++ checking whether the C++ compiler works... yes checking for C++ compiler default output file name... a.out checking for suffix of executables... checking whether we are cross compiling... no checking for suffix of object files... o checking whether we are using the GNU C++ compiler... yes checking whether g++ accepts -g... yes checking how to run the C++ preprocessor... g++ -E checking for ar... ar checking build system type... x86_64-pc-linux-gnu checking host system type... x86_64-pc-linux-gnu checking for install... /usr/bin/install checking for ldconfig... /sbin/ldconfig checking for time... not found configure: WARNING: Regression tests depend upon GNU time. checking for perl... /usr/bin/perl checking for bison... bison -y checking for flex... flex checking lex output file root... lex.yy checking lex library... none needed checking whether yytext is a pointer... no checking for compiler version (g++ --version)... 5.2.1 checking for gmp... yes checking for javac... /usr/lib/jvm/default-java/bin/javac checking for javah... /usr/lib/jvm/default-java/bin/javah checking for jar... /usr/lib/jvm/default-java/bin/jar checking for java... /usr/lib/jvm/default-java/bin/java checking for grep that handles long lines and -e... /bin/grep checking for egrep... /bin/grep -E checking for ANSI C header files... yes checking for sys/types.h... yes checking for sys/stat.h... yes checking for stdlib.h... yes checking for string.h... yes checking for memory.h... yes checking for strings.h... yes checking for inttypes.h... yes checking for stdint.h... yes checking for unistd.h... yes checking jni.h usability... yes checking jni.h presence... yes checking for jni.h... yes checking jni_md.h usability... yes checking jni_md.h presence... yes checking for jni_md.h... yes checking for python... /usr/bin/python checking vector usability... yes checking vector presence... yes checking for vector... yes checking list usability... yes checking list presence... yes checking for list... yes checking deque usability... yes checking deque presence... yes checking for deque... yes checking set usability... yes checking set presence... yes checking for set... yes checking string usability... yes checking string presence... yes checking for string... yes checking cstdlib usability... yes checking cstdlib presence... yes checking for cstdlib... yes checking cstdio usability... yes checking cstdio presence... yes checking for cstdio... yes checking functional usability... yes checking functional presence... yes checking for functional... yes checking algorithm usability... yes checking algorithm presence... yes checking for algorithm... yes checking for doxygen... no checking for doxytag... no checking for fig2dev... no checking for dot... NO checking for etags... no checking for ebrowse... no configure: creating ./config.status config.status: creating Makefile.local config.status: creating LICENSE config.status: creating src/cvc3.pc config.status: creating bin/unpack config.status: creating bin/run_tests config.status: creating bin/cvc2smt config.status: creating doc/Doxyfile config.status: creating doc/Makefile configure: WARNING: unrecognized options: --disable-maintainer-mode, --disable-dependency-tracking, --disable-silent-rules CVC3 is configured successfully. Platform: x86_64-linux-gnu Version: 2.4.1 Computer arithmetic: GMP Run ./configure --help for additional configuration options. Type 'make' to compile CVC3. *** CVC3 is configured to compile using shared libraries. *** Type "make ld_sh" for bash shells or "make ld_csh" for csh shells *** to see how to set LD_LIBRARY_PATH appropriately. To use static *** libraries and executables instead, run: *** ./configure --enable-static touch debian/stamp-autotools /usr/bin/make -C . make[1]: Entering directory '/cvc3-2.4.1' cd /cvc3-2.4.1/src; /usr/bin/make VERSION=2.4.1 make[2]: Entering directory '/cvc3-2.4.1/src' cd util && /usr/bin/make make[3]: Entering directory '/cvc3-2.4.1/src/util' Making dependencies for debug.cpp statistics.cpp rational.cpp rational-native.cpp rational-gmp.cpp g++ -M -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -DRATIONAL_GMP -D_FORTIFY_SOURCE=2 debug.cpp statistics.cpp rational.cpp rational-native.cpp rational-gmp.cpp >> /cvc3-2.4.1/obj/util/x86_64-linux-gnu/Makefile.tmp g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -DRATIONAL_GMP -D_FORTIFY_SOURCE=2 -c debug.cpp -o '/cvc3-2.4.1/obj/util/x86_64-linux-gnu/debug.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -DRATIONAL_GMP -D_FORTIFY_SOURCE=2 -c statistics.cpp -o '/cvc3-2.4.1/obj/util/x86_64-linux-gnu/statistics.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -DRATIONAL_GMP -D_FORTIFY_SOURCE=2 -c rational.cpp -o '/cvc3-2.4.1/obj/util/x86_64-linux-gnu/rational.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -DRATIONAL_GMP -D_FORTIFY_SOURCE=2 -c rational-native.cpp -o '/cvc3-2.4.1/obj/util/x86_64-linux-gnu/rational-native.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -DRATIONAL_GMP -D_FORTIFY_SOURCE=2 -c rational-gmp.cpp -o '/cvc3-2.4.1/obj/util/x86_64-linux-gnu/rational-gmp.o' ar ruvs '/cvc3-2.4.1/lib/x86_64-linux-gnu/libcvc_util.a' /cvc3-2.4.1/obj/util/x86_64-linux-gnu/debug.o /cvc3-2.4.1/obj/util/x86_64-linux-gnu/statistics.o /cvc3-2.4.1/obj/util/x86_64-linux-gnu/rational.o /cvc3-2.4.1/obj/util/x86_64-linux-gnu/rational-native.o /cvc3-2.4.1/obj/util/x86_64-linux-gnu/rational-gmp.o ar: `u' modifier ignored since `D' is the default (see `U') ar: creating /cvc3-2.4.1/lib/x86_64-linux-gnu/libcvc_util.a a - /cvc3-2.4.1/obj/util/x86_64-linux-gnu/debug.o a - /cvc3-2.4.1/obj/util/x86_64-linux-gnu/statistics.o a - /cvc3-2.4.1/obj/util/x86_64-linux-gnu/rational.o a - /cvc3-2.4.1/obj/util/x86_64-linux-gnu/rational-native.o a - /cvc3-2.4.1/obj/util/x86_64-linux-gnu/rational-gmp.o make[3]: Leaving directory '/cvc3-2.4.1/src/util' cd context && /usr/bin/make make[3]: Entering directory '/cvc3-2.4.1/src/context' Making dependencies for context.cpp cdflags.cpp g++ -M -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 context.cpp cdflags.cpp >> /cvc3-2.4.1/obj/context/x86_64-linux-gnu/Makefile.tmp g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c context.cpp -o '/cvc3-2.4.1/obj/context/x86_64-linux-gnu/context.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c cdflags.cpp -o '/cvc3-2.4.1/obj/context/x86_64-linux-gnu/cdflags.o' ar ruvs '/cvc3-2.4.1/lib/x86_64-linux-gnu/libcontext.a' /cvc3-2.4.1/obj/context/x86_64-linux-gnu/context.o /cvc3-2.4.1/obj/context/x86_64-linux-gnu/cdflags.o ar: `u' modifier ignored since `D' is the default (see `U') ar: creating /cvc3-2.4.1/lib/x86_64-linux-gnu/libcontext.a a - /cvc3-2.4.1/obj/context/x86_64-linux-gnu/context.o a - /cvc3-2.4.1/obj/context/x86_64-linux-gnu/cdflags.o make[3]: Leaving directory '/cvc3-2.4.1/src/context' cd expr && /usr/bin/make make[3]: Entering directory '/cvc3-2.4.1/src/expr' Making dependencies for expr.cpp expr_manager.cpp expr_stream.cpp expr_value.cpp expr_op.cpp g++ -M -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 expr.cpp expr_manager.cpp expr_stream.cpp expr_value.cpp expr_op.cpp >> /cvc3-2.4.1/obj/expr/x86_64-linux-gnu/Makefile.tmp g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c expr.cpp -o '/cvc3-2.4.1/obj/expr/x86_64-linux-gnu/expr.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c expr_manager.cpp -o '/cvc3-2.4.1/obj/expr/x86_64-linux-gnu/expr_manager.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c expr_stream.cpp -o '/cvc3-2.4.1/obj/expr/x86_64-linux-gnu/expr_stream.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c expr_value.cpp -o '/cvc3-2.4.1/obj/expr/x86_64-linux-gnu/expr_value.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c expr_op.cpp -o '/cvc3-2.4.1/obj/expr/x86_64-linux-gnu/expr_op.o' ar ruvs '/cvc3-2.4.1/lib/x86_64-linux-gnu/libexpr.a' /cvc3-2.4.1/obj/expr/x86_64-linux-gnu/expr.o /cvc3-2.4.1/obj/expr/x86_64-linux-gnu/expr_manager.o /cvc3-2.4.1/obj/expr/x86_64-linux-gnu/expr_stream.o /cvc3-2.4.1/obj/expr/x86_64-linux-gnu/expr_value.o /cvc3-2.4.1/obj/expr/x86_64-linux-gnu/expr_op.o ar: `u' modifier ignored since `D' is the default (see `U') ar: creating /cvc3-2.4.1/lib/x86_64-linux-gnu/libexpr.a a - /cvc3-2.4.1/obj/expr/x86_64-linux-gnu/expr.o a - /cvc3-2.4.1/obj/expr/x86_64-linux-gnu/expr_manager.o a - /cvc3-2.4.1/obj/expr/x86_64-linux-gnu/expr_stream.o a - /cvc3-2.4.1/obj/expr/x86_64-linux-gnu/expr_value.o a - /cvc3-2.4.1/obj/expr/x86_64-linux-gnu/expr_op.o make[3]: Leaving directory '/cvc3-2.4.1/src/expr' cd theorem && /usr/bin/make make[3]: Entering directory '/cvc3-2.4.1/src/theorem' Making dependencies for assumptions.cpp theorem.cpp theorem_manager.cpp theorem_producer.cpp common_theorem_producer.cpp g++ -M -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 assumptions.cpp theorem.cpp theorem_manager.cpp theorem_producer.cpp common_theorem_producer.cpp >> /cvc3-2.4.1/obj/theorem/x86_64-linux-gnu/Makefile.tmp g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c assumptions.cpp -o '/cvc3-2.4.1/obj/theorem/x86_64-linux-gnu/assumptions.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c theorem.cpp -o '/cvc3-2.4.1/obj/theorem/x86_64-linux-gnu/theorem.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c theorem_manager.cpp -o '/cvc3-2.4.1/obj/theorem/x86_64-linux-gnu/theorem_manager.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c theorem_producer.cpp -o '/cvc3-2.4.1/obj/theorem/x86_64-linux-gnu/theorem_producer.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c common_theorem_producer.cpp -o '/cvc3-2.4.1/obj/theorem/x86_64-linux-gnu/common_theorem_producer.o' In file included from common_theorem_producer.h:34:0, from common_theorem_producer.cpp:27: common_theorem_producer.cpp: In member function ‘virtual CVC3::Theorem CVC3::CommonTheoremProducer::contradictionRule(const CVC3::Theorem&, const CVC3::Theorem&)’: common_theorem_producer.cpp:565:30: warning: logical not is only applied to the left hand side of comparison [-Wlogical-not-parentheses] CHECK_SOUND(!e.getExpr() == not_e.getExpr(), ^ /cvc3-2.4.1/src/include/theorem_producer.h:83:39: note: in definition of macro ‘CHECK_SOUND’ #define CHECK_SOUND(cond, msg) { if(!(cond)) \ ^ ar ruvs '/cvc3-2.4.1/lib/x86_64-linux-gnu/libtheorem.a' /cvc3-2.4.1/obj/theorem/x86_64-linux-gnu/assumptions.o /cvc3-2.4.1/obj/theorem/x86_64-linux-gnu/theorem.o /cvc3-2.4.1/obj/theorem/x86_64-linux-gnu/theorem_manager.o /cvc3-2.4.1/obj/theorem/x86_64-linux-gnu/theorem_producer.o /cvc3-2.4.1/obj/theorem/x86_64-linux-gnu/common_theorem_producer.o ar: `u' modifier ignored since `D' is the default (see `U') ar: creating /cvc3-2.4.1/lib/x86_64-linux-gnu/libtheorem.a a - /cvc3-2.4.1/obj/theorem/x86_64-linux-gnu/assumptions.o a - /cvc3-2.4.1/obj/theorem/x86_64-linux-gnu/theorem.o a - /cvc3-2.4.1/obj/theorem/x86_64-linux-gnu/theorem_manager.o a - /cvc3-2.4.1/obj/theorem/x86_64-linux-gnu/theorem_producer.o a - /cvc3-2.4.1/obj/theorem/x86_64-linux-gnu/common_theorem_producer.o make[3]: Leaving directory '/cvc3-2.4.1/src/theorem' cd sat && /usr/bin/make make[3]: Entering directory '/cvc3-2.4.1/src/sat' Making dependencies for cnf.cpp cnf_manager.cpp cnf_theorem_producer.cpp dpllt_basic.cpp sat_api.cpp dpllt_minisat.cpp minisat_types.cpp minisat_derivation.cpp minisat_solver.cpp g++ -M -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 cnf.cpp cnf_manager.cpp cnf_theorem_producer.cpp dpllt_basic.cpp sat_api.cpp dpllt_minisat.cpp minisat_types.cpp minisat_derivation.cpp minisat_solver.cpp >> /cvc3-2.4.1/obj/sat/x86_64-linux-gnu/Makefile.tmp g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c cnf.cpp -o '/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/cnf.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c cnf_manager.cpp -o '/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/cnf_manager.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c cnf_theorem_producer.cpp -o '/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/cnf_theorem_producer.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c dpllt_basic.cpp -o '/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/dpllt_basic.o' dpllt_basic.cpp: In member function ‘void SAT::DPLLTBasic::handle_result(SatSolver::SATStatus)’: dpllt_basic.cpp:172:16: warning: variable ‘result’ set but not used [-Wunused-but-set-variable] const char * result = "UNKNOWN"; ^ g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c sat_api.cpp -o '/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/sat_api.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c dpllt_minisat.cpp -o '/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/dpllt_minisat.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c minisat_types.cpp -o '/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/minisat_types.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c minisat_derivation.cpp -o '/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/minisat_derivation.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c minisat_solver.cpp -o '/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/minisat_solver.o' ar ruvs '/cvc3-2.4.1/lib/x86_64-linux-gnu/libsat.a' /cvc3-2.4.1/obj/sat/x86_64-linux-gnu/cnf.o /cvc3-2.4.1/obj/sat/x86_64-linux-gnu/cnf_manager.o /cvc3-2.4.1/obj/sat/x86_64-linux-gnu/cnf_theorem_producer.o /cvc3-2.4.1/obj/sat/x86_64-linux-gnu/dpllt_basic.o /cvc3-2.4.1/obj/sat/x86_64-linux-gnu/sat_api.o /cvc3-2.4.1/obj/sat/x86_64-linux-gnu/dpllt_minisat.o /cvc3-2.4.1/obj/sat/x86_64-linux-gnu/minisat_types.o /cvc3-2.4.1/obj/sat/x86_64-linux-gnu/minisat_derivation.o /cvc3-2.4.1/obj/sat/x86_64-linux-gnu/minisat_solver.o ar: `u' modifier ignored since `D' is the default (see `U') ar: creating /cvc3-2.4.1/lib/x86_64-linux-gnu/libsat.a a - /cvc3-2.4.1/obj/sat/x86_64-linux-gnu/cnf.o a - /cvc3-2.4.1/obj/sat/x86_64-linux-gnu/cnf_manager.o a - /cvc3-2.4.1/obj/sat/x86_64-linux-gnu/cnf_theorem_producer.o a - /cvc3-2.4.1/obj/sat/x86_64-linux-gnu/dpllt_basic.o a - /cvc3-2.4.1/obj/sat/x86_64-linux-gnu/sat_api.o a - /cvc3-2.4.1/obj/sat/x86_64-linux-gnu/dpllt_minisat.o a - /cvc3-2.4.1/obj/sat/x86_64-linux-gnu/minisat_types.o a - /cvc3-2.4.1/obj/sat/x86_64-linux-gnu/minisat_derivation.o a - /cvc3-2.4.1/obj/sat/x86_64-linux-gnu/minisat_solver.o make[3]: Leaving directory '/cvc3-2.4.1/src/sat' cd theory_core && /usr/bin/make make[3]: Entering directory '/cvc3-2.4.1/src/theory_core' Making dependencies for theory.cpp theory_core.cpp core_theorem_producer.cpp expr_transform.cpp bryant.cpp g++ -M -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 theory.cpp theory_core.cpp core_theorem_producer.cpp expr_transform.cpp bryant.cpp >> /cvc3-2.4.1/obj/theory_core/x86_64-linux-gnu/Makefile.tmp g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c theory.cpp -o '/cvc3-2.4.1/obj/theory_core/x86_64-linux-gnu/theory.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c theory_core.cpp -o '/cvc3-2.4.1/obj/theory_core/x86_64-linux-gnu/theory_core.o' theory_core.cpp: In constructor ‘CVC3::TheoryCore::TheoryCore(CVC3::ContextManager*, CVC3::ExprManager*, CVC3::TheoremManager*, CVC3::Translator*, const CVC3::CLFlags&, CVC3::Statistics&)’: theory_core.cpp:725:22: warning: converting ‘false’ to pointer type ‘const bool*’ [-Wconversion-null] d_coreSatAPI(NULL) ^ g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c core_theorem_producer.cpp -o '/cvc3-2.4.1/obj/theory_core/x86_64-linux-gnu/core_theorem_producer.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c expr_transform.cpp -o '/cvc3-2.4.1/obj/theory_core/x86_64-linux-gnu/expr_transform.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c bryant.cpp -o '/cvc3-2.4.1/obj/theory_core/x86_64-linux-gnu/bryant.o' bryant.cpp: In member function ‘CVC3::Expr CVC3::ExprTransform::ConstrainedConstraints(std::set&, CVC3::ExprTransform::T_generator_map&, CVC3::ExprTransform::B_name_map&, CVC3::ExprTransform::B_Term_map&, std::set&, std::set&, std::set&)’: bryant.cpp:470:17: warning: logical not is only applied to the left hand side of comparison [-Wlogical-not-parentheses] if (!Value == Temp) ^ ar ruvs '/cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_core.a' /cvc3-2.4.1/obj/theory_core/x86_64-linux-gnu/theory.o /cvc3-2.4.1/obj/theory_core/x86_64-linux-gnu/theory_core.o /cvc3-2.4.1/obj/theory_core/x86_64-linux-gnu/core_theorem_producer.o /cvc3-2.4.1/obj/theory_core/x86_64-linux-gnu/expr_transform.o /cvc3-2.4.1/obj/theory_core/x86_64-linux-gnu/bryant.o ar: `u' modifier ignored since `D' is the default (see `U') ar: creating /cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_core.a a - /cvc3-2.4.1/obj/theory_core/x86_64-linux-gnu/theory.o a - /cvc3-2.4.1/obj/theory_core/x86_64-linux-gnu/theory_core.o a - /cvc3-2.4.1/obj/theory_core/x86_64-linux-gnu/core_theorem_producer.o a - /cvc3-2.4.1/obj/theory_core/x86_64-linux-gnu/expr_transform.o a - /cvc3-2.4.1/obj/theory_core/x86_64-linux-gnu/bryant.o make[3]: Leaving directory '/cvc3-2.4.1/src/theory_core' cd theory_arith && /usr/bin/make make[3]: Entering directory '/cvc3-2.4.1/src/theory_arith' Making dependencies for arith_theorem_producer_old.cpp arith_theorem_producer.cpp arith_theorem_producer3.cpp theory_arith.cpp theory_arith_old.cpp theory_arith_new.cpp theory_arith3.cpp g++ -M -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 arith_theorem_producer_old.cpp arith_theorem_producer.cpp arith_theorem_producer3.cpp theory_arith.cpp theory_arith_old.cpp theory_arith_new.cpp theory_arith3.cpp >> /cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/Makefile.tmp g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c arith_theorem_producer_old.cpp -o '/cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer_old.o' arith_theorem_producer_old.cpp: In member function ‘virtual CVC3::Theorem CVC3::ArithTheoremProducerOld::canonMult(const CVC3::Expr&)’: arith_theorem_producer_old.cpp:797:50: warning: logical not is only applied to the left hand side of comparison [-Wlogical-not-parentheses] if (count_non_trivial > 0 && !count_constants == (e.arity() - 1)) { ^ g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c arith_theorem_producer.cpp -o '/cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c arith_theorem_producer3.cpp -o '/cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer3.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c theory_arith.cpp -o '/cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/theory_arith.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c theory_arith_old.cpp -o '/cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/theory_arith_old.o' theory_arith_old.cpp: In member function ‘bool CVC3::TheoryArithOld::findBounds(const CVC3::Expr&, CVC3::Rational&, CVC3::Rational&)’: theory_arith_old.cpp:2782:24: warning: variable ‘strictUB’ set but not used [-Wunused-but-set-variable] bool strictLB=false, strictUB=false; ^ g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c theory_arith_new.cpp -o '/cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/theory_arith_new.o' theory_arith_new.cpp: In member function ‘bool CVC3::TheoryArithNew::findBounds(const CVC3::Expr&, CVC3::Rational&, CVC3::Rational&)’: theory_arith_new.cpp:1350:24: warning: variable ‘strictUB’ set but not used [-Wunused-but-set-variable] bool strictLB=false, strictUB=false; ^ g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c theory_arith3.cpp -o '/cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/theory_arith3.o' theory_arith3.cpp: In member function ‘bool CVC3::TheoryArith3::findBounds(const CVC3::Expr&, CVC3::Rational&, CVC3::Rational&)’: theory_arith3.cpp:2199:24: warning: variable ‘strictUB’ set but not used [-Wunused-but-set-variable] bool strictLB=false, strictUB=false; ^ ar ruvs '/cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_arith.a' /cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer_old.o /cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer.o /cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer3.o /cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/theory_arith.o /cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/theory_arith_old.o /cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/theory_arith_new.o /cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/theory_arith3.o ar: `u' modifier ignored since `D' is the default (see `U') ar: creating /cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_arith.a a - /cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer_old.o a - /cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer.o a - /cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer3.o a - /cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/theory_arith.o a - /cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/theory_arith_old.o a - /cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/theory_arith_new.o a - /cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/theory_arith3.o make[3]: Leaving directory '/cvc3-2.4.1/src/theory_arith' cd theory_array && /usr/bin/make make[3]: Entering directory '/cvc3-2.4.1/src/theory_array' Making dependencies for array_theorem_producer.cpp theory_array.cpp g++ -M -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 array_theorem_producer.cpp theory_array.cpp >> /cvc3-2.4.1/obj/theory_array/x86_64-linux-gnu/Makefile.tmp g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c array_theorem_producer.cpp -o '/cvc3-2.4.1/obj/theory_array/x86_64-linux-gnu/array_theorem_producer.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c theory_array.cpp -o '/cvc3-2.4.1/obj/theory_array/x86_64-linux-gnu/theory_array.o' ar ruvs '/cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_array.a' /cvc3-2.4.1/obj/theory_array/x86_64-linux-gnu/array_theorem_producer.o /cvc3-2.4.1/obj/theory_array/x86_64-linux-gnu/theory_array.o ar: `u' modifier ignored since `D' is the default (see `U') ar: creating /cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_array.a a - /cvc3-2.4.1/obj/theory_array/x86_64-linux-gnu/array_theorem_producer.o a - /cvc3-2.4.1/obj/theory_array/x86_64-linux-gnu/theory_array.o make[3]: Leaving directory '/cvc3-2.4.1/src/theory_array' cd theory_bitvector && /usr/bin/make make[3]: Entering directory '/cvc3-2.4.1/src/theory_bitvector' Making dependencies for bitvector_theorem_producer.cpp theory_bitvector.cpp g++ -M -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 bitvector_theorem_producer.cpp theory_bitvector.cpp >> /cvc3-2.4.1/obj/theory_bitvector/x86_64-linux-gnu/Makefile.tmp g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c bitvector_theorem_producer.cpp -o '/cvc3-2.4.1/obj/theory_bitvector/x86_64-linux-gnu/bitvector_theorem_producer.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c theory_bitvector.cpp -o '/cvc3-2.4.1/obj/theory_bitvector/x86_64-linux-gnu/theory_bitvector.o' theory_bitvector.cpp: In member function ‘CVC3::Theorem CVC3::TheoryBitvector::rewriteBV(const CVC3::Expr&, CVC3::ExprMap&, int)’: theory_bitvector.cpp:1063:11: warning: variable ‘hi’ set but not used [-Wunused-but-set-variable] int hi(-1), low(-1); ^ ar ruvs '/cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_bitvector.a' /cvc3-2.4.1/obj/theory_bitvector/x86_64-linux-gnu/bitvector_theorem_producer.o /cvc3-2.4.1/obj/theory_bitvector/x86_64-linux-gnu/theory_bitvector.o ar: `u' modifier ignored since `D' is the default (see `U') ar: creating /cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_bitvector.a a - /cvc3-2.4.1/obj/theory_bitvector/x86_64-linux-gnu/bitvector_theorem_producer.o a - /cvc3-2.4.1/obj/theory_bitvector/x86_64-linux-gnu/theory_bitvector.o make[3]: Leaving directory '/cvc3-2.4.1/src/theory_bitvector' cd theory_datatype && /usr/bin/make make[3]: Entering directory '/cvc3-2.4.1/src/theory_datatype' Making dependencies for datatype_theorem_producer.cpp theory_datatype.cpp theory_datatype_lazy.cpp g++ -M -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 datatype_theorem_producer.cpp theory_datatype.cpp theory_datatype_lazy.cpp >> /cvc3-2.4.1/obj/theory_datatype/x86_64-linux-gnu/Makefile.tmp g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c datatype_theorem_producer.cpp -o '/cvc3-2.4.1/obj/theory_datatype/x86_64-linux-gnu/datatype_theorem_producer.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c theory_datatype.cpp -o '/cvc3-2.4.1/obj/theory_datatype/x86_64-linux-gnu/theory_datatype.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c theory_datatype_lazy.cpp -o '/cvc3-2.4.1/obj/theory_datatype/x86_64-linux-gnu/theory_datatype_lazy.o' ar ruvs '/cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_datatype.a' /cvc3-2.4.1/obj/theory_datatype/x86_64-linux-gnu/datatype_theorem_producer.o /cvc3-2.4.1/obj/theory_datatype/x86_64-linux-gnu/theory_datatype.o /cvc3-2.4.1/obj/theory_datatype/x86_64-linux-gnu/theory_datatype_lazy.o ar: `u' modifier ignored since `D' is the default (see `U') ar: creating /cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_datatype.a a - /cvc3-2.4.1/obj/theory_datatype/x86_64-linux-gnu/datatype_theorem_producer.o a - /cvc3-2.4.1/obj/theory_datatype/x86_64-linux-gnu/theory_datatype.o a - /cvc3-2.4.1/obj/theory_datatype/x86_64-linux-gnu/theory_datatype_lazy.o make[3]: Leaving directory '/cvc3-2.4.1/src/theory_datatype' cd theory_quant && /usr/bin/make make[3]: Entering directory '/cvc3-2.4.1/src/theory_quant' Making dependencies for theory_quant.cpp quant_theorem_producer.cpp g++ -M -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 theory_quant.cpp quant_theorem_producer.cpp >> /cvc3-2.4.1/obj/theory_quant/x86_64-linux-gnu/Makefile.tmp g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c theory_quant.cpp -o '/cvc3-2.4.1/obj/theory_quant/x86_64-linux-gnu/theory_quant.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c quant_theorem_producer.cpp -o '/cvc3-2.4.1/obj/theory_quant/x86_64-linux-gnu/quant_theorem_producer.o' ar ruvs '/cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_quant.a' /cvc3-2.4.1/obj/theory_quant/x86_64-linux-gnu/theory_quant.o /cvc3-2.4.1/obj/theory_quant/x86_64-linux-gnu/quant_theorem_producer.o ar: `u' modifier ignored since `D' is the default (see `U') ar: creating /cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_quant.a a - /cvc3-2.4.1/obj/theory_quant/x86_64-linux-gnu/theory_quant.o a - /cvc3-2.4.1/obj/theory_quant/x86_64-linux-gnu/quant_theorem_producer.o make[3]: Leaving directory '/cvc3-2.4.1/src/theory_quant' cd theory_records && /usr/bin/make make[3]: Entering directory '/cvc3-2.4.1/src/theory_records' Making dependencies for theory_records.cpp records_theorem_producer.cpp g++ -M -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 theory_records.cpp records_theorem_producer.cpp >> /cvc3-2.4.1/obj/theory_records/x86_64-linux-gnu/Makefile.tmp g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c theory_records.cpp -o '/cvc3-2.4.1/obj/theory_records/x86_64-linux-gnu/theory_records.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c records_theorem_producer.cpp -o '/cvc3-2.4.1/obj/theory_records/x86_64-linux-gnu/records_theorem_producer.o' ar ruvs '/cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_records.a' /cvc3-2.4.1/obj/theory_records/x86_64-linux-gnu/theory_records.o /cvc3-2.4.1/obj/theory_records/x86_64-linux-gnu/records_theorem_producer.o ar: `u' modifier ignored since `D' is the default (see `U') ar: creating /cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_records.a a - /cvc3-2.4.1/obj/theory_records/x86_64-linux-gnu/theory_records.o a - /cvc3-2.4.1/obj/theory_records/x86_64-linux-gnu/records_theorem_producer.o make[3]: Leaving directory '/cvc3-2.4.1/src/theory_records' cd theory_simulate && /usr/bin/make make[3]: Entering directory '/cvc3-2.4.1/src/theory_simulate' Making dependencies for theory_simulate.cpp simulate_theorem_producer.cpp g++ -M -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 theory_simulate.cpp simulate_theorem_producer.cpp >> /cvc3-2.4.1/obj/theory_simulate/x86_64-linux-gnu/Makefile.tmp g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c theory_simulate.cpp -o '/cvc3-2.4.1/obj/theory_simulate/x86_64-linux-gnu/theory_simulate.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c simulate_theorem_producer.cpp -o '/cvc3-2.4.1/obj/theory_simulate/x86_64-linux-gnu/simulate_theorem_producer.o' ar ruvs '/cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_simulate.a' /cvc3-2.4.1/obj/theory_simulate/x86_64-linux-gnu/theory_simulate.o /cvc3-2.4.1/obj/theory_simulate/x86_64-linux-gnu/simulate_theorem_producer.o ar: `u' modifier ignored since `D' is the default (see `U') ar: creating /cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_simulate.a a - /cvc3-2.4.1/obj/theory_simulate/x86_64-linux-gnu/theory_simulate.o a - /cvc3-2.4.1/obj/theory_simulate/x86_64-linux-gnu/simulate_theorem_producer.o make[3]: Leaving directory '/cvc3-2.4.1/src/theory_simulate' cd theory_uf && /usr/bin/make make[3]: Entering directory '/cvc3-2.4.1/src/theory_uf' Making dependencies for uf_theorem_producer.cpp theory_uf.cpp g++ -M -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 uf_theorem_producer.cpp theory_uf.cpp >> /cvc3-2.4.1/obj/theory_uf/x86_64-linux-gnu/Makefile.tmp g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c uf_theorem_producer.cpp -o '/cvc3-2.4.1/obj/theory_uf/x86_64-linux-gnu/uf_theorem_producer.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c theory_uf.cpp -o '/cvc3-2.4.1/obj/theory_uf/x86_64-linux-gnu/theory_uf.o' ar ruvs '/cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_uf.a' /cvc3-2.4.1/obj/theory_uf/x86_64-linux-gnu/uf_theorem_producer.o /cvc3-2.4.1/obj/theory_uf/x86_64-linux-gnu/theory_uf.o ar: `u' modifier ignored since `D' is the default (see `U') ar: creating /cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_uf.a a - /cvc3-2.4.1/obj/theory_uf/x86_64-linux-gnu/uf_theorem_producer.o a - /cvc3-2.4.1/obj/theory_uf/x86_64-linux-gnu/theory_uf.o make[3]: Leaving directory '/cvc3-2.4.1/src/theory_uf' cd search && /usr/bin/make make[3]: Entering directory '/cvc3-2.4.1/src/search' Making dependencies for clause.cpp search_impl_base.cpp search.cpp search_fast.cpp search_theorem_producer.cpp search_sat.cpp search_simple.cpp variable.cpp circuit.cpp decision_engine.cpp decision_engine_dfs.cpp LFSCObject.cpp LFSCUtilProof.cpp LFSCBoolProof.cpp LFSCConvert.cpp LFSCLraProof.cpp LFSCPrinter.cpp LFSCProof.cpp TReturn.cpp Util.cpp g++ -M -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 clause.cpp search_impl_base.cpp search.cpp search_fast.cpp search_theorem_producer.cpp search_sat.cpp search_simple.cpp variable.cpp circuit.cpp decision_engine.cpp decision_engine_dfs.cpp LFSCObject.cpp LFSCUtilProof.cpp LFSCBoolProof.cpp LFSCConvert.cpp LFSCLraProof.cpp LFSCPrinter.cpp LFSCProof.cpp TReturn.cpp Util.cpp >> /cvc3-2.4.1/obj/search/x86_64-linux-gnu/Makefile.tmp g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c clause.cpp -o '/cvc3-2.4.1/obj/search/x86_64-linux-gnu/clause.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c search_impl_base.cpp -o '/cvc3-2.4.1/obj/search/x86_64-linux-gnu/search_impl_base.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c search.cpp -o '/cvc3-2.4.1/obj/search/x86_64-linux-gnu/search.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c search_fast.cpp -o '/cvc3-2.4.1/obj/search/x86_64-linux-gnu/search_fast.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c search_theorem_producer.cpp -o '/cvc3-2.4.1/obj/search/x86_64-linux-gnu/search_theorem_producer.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c search_sat.cpp -o '/cvc3-2.4.1/obj/search/x86_64-linux-gnu/search_sat.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c search_simple.cpp -o '/cvc3-2.4.1/obj/search/x86_64-linux-gnu/search_simple.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c variable.cpp -o '/cvc3-2.4.1/obj/search/x86_64-linux-gnu/variable.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c circuit.cpp -o '/cvc3-2.4.1/obj/search/x86_64-linux-gnu/circuit.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c decision_engine.cpp -o '/cvc3-2.4.1/obj/search/x86_64-linux-gnu/decision_engine.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c decision_engine_dfs.cpp -o '/cvc3-2.4.1/obj/search/x86_64-linux-gnu/decision_engine_dfs.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c LFSCObject.cpp -o '/cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCObject.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c LFSCUtilProof.cpp -o '/cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCUtilProof.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c LFSCBoolProof.cpp -o '/cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCBoolProof.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c LFSCConvert.cpp -o '/cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCConvert.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c LFSCLraProof.cpp -o '/cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCLraProof.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c LFSCPrinter.cpp -o '/cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCPrinter.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c LFSCProof.cpp -o '/cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCProof.o' LFSCProof.cpp: In member function ‘virtual int LFSCProof::checkOp()’: LFSCProof.cpp:91:11: warning: unused variable ‘o’ [-Wunused-variable] int o = getChild( a )->checkOp(); ^ LFSCProof.cpp: In static member function ‘static LFSCProof* LFSCProof::Make_CNF(const CVC3::Expr&, const CVC3::Expr&, int)’: LFSCProof.cpp:193:11: warning: unused variable ‘m2’ [-Wunused-variable] int m2 = queryM( ec[1] ); ^ g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c TReturn.cpp -o '/cvc3-2.4.1/obj/search/x86_64-linux-gnu/TReturn.o' TReturn.cpp: In static member function ‘static int TReturn::normalize_tr(const CVC3::Expr&, TReturn*&, int, bool, bool)’: TReturn.cpp:127:12: warning: unused variable ‘torig’ [-Wunused-variable] TReturn* torig = t1; ^ g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c Util.cpp -o '/cvc3-2.4.1/obj/search/x86_64-linux-gnu/Util.o' ar ruvs '/cvc3-2.4.1/lib/x86_64-linux-gnu/libsearch.a' /cvc3-2.4.1/obj/search/x86_64-linux-gnu/clause.o /cvc3-2.4.1/obj/search/x86_64-linux-gnu/search_impl_base.o /cvc3-2.4.1/obj/search/x86_64-linux-gnu/search.o /cvc3-2.4.1/obj/search/x86_64-linux-gnu/search_fast.o /cvc3-2.4.1/obj/search/x86_64-linux-gnu/search_theorem_producer.o /cvc3-2.4.1/obj/search/x86_64-linux-gnu/search_sat.o /cvc3-2.4.1/obj/search/x86_64-linux-gnu/search_simple.o /cvc3-2.4.1/obj/search/x86_64-linux-gnu/variable.o /cvc3-2.4.1/obj/search/x86_64-linux-gnu/circuit.o /cvc3-2.4.1/obj/search/x86_64-linux-gnu/decision_engine.o /cvc3-2.4.1/obj/search/x86_64-linux-gnu/decision_engine_dfs.o /cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCObject.o /cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCUtilProof.o /cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCBoolProof.o /cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCConvert.o /cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCLraProof.o /cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCPrinter.o /cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCProof.o /cvc3-2.4.1/obj/search/x86_64-linux-gnu/TReturn.o /cvc3-2.4.1/obj/search/x86_64-linux-gnu/Util.o ar: `u' modifier ignored since `D' is the default (see `U') ar: creating /cvc3-2.4.1/lib/x86_64-linux-gnu/libsearch.a a - /cvc3-2.4.1/obj/search/x86_64-linux-gnu/clause.o a - /cvc3-2.4.1/obj/search/x86_64-linux-gnu/search_impl_base.o a - /cvc3-2.4.1/obj/search/x86_64-linux-gnu/search.o a - /cvc3-2.4.1/obj/search/x86_64-linux-gnu/search_fast.o a - /cvc3-2.4.1/obj/search/x86_64-linux-gnu/search_theorem_producer.o a - /cvc3-2.4.1/obj/search/x86_64-linux-gnu/search_sat.o a - /cvc3-2.4.1/obj/search/x86_64-linux-gnu/search_simple.o a - /cvc3-2.4.1/obj/search/x86_64-linux-gnu/variable.o a - /cvc3-2.4.1/obj/search/x86_64-linux-gnu/circuit.o a - /cvc3-2.4.1/obj/search/x86_64-linux-gnu/decision_engine.o a - /cvc3-2.4.1/obj/search/x86_64-linux-gnu/decision_engine_dfs.o a - /cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCObject.o a - /cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCUtilProof.o a - /cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCBoolProof.o a - /cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCConvert.o a - /cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCLraProof.o a - /cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCPrinter.o a - /cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCProof.o a - /cvc3-2.4.1/obj/search/x86_64-linux-gnu/TReturn.o a - /cvc3-2.4.1/obj/search/x86_64-linux-gnu/Util.o make[3]: Leaving directory '/cvc3-2.4.1/src/search' cd parser && /usr/bin/make make[3]: Entering directory '/cvc3-2.4.1/src/parser' bison -d -y -o parsePL.cpp -p PL --debug -v PL.y PL.y: warning: 3 shift/reduce conflicts [-Wconflicts-sr] PL.y:1531.24-1536.25: warning: rule useless in parser due to conflicts [-Wother] AndExpr : AndExpr AND_TOK Expr ^^^^^^^^^^^^^ PL.y:1549.25-1554.25: warning: rule useless in parser due to conflicts [-Wother] OrExpr : OrExpr OR_TOK Expr ^^^^^^^^^^ flex -I -PPL -olexPL.cpp PL.lex bison -d -y -o parseLisp.cpp -p Lisp --debug -v Lisp.y flex -I -PLisp -olexLisp.cpp Lisp.lex bison -d -y -o parsesmtlib.cpp -p smtlib --debug -v smtlib.y flex -I -Psmtlib -olexsmtlib.cpp smtlib.lex bison -d -y -o parsesmtlib2.cpp -p smtlib2 --debug -v smtlib2.y smtlib2.y: warning: 4 shift/reduce conflicts [-Wconflicts-sr] flex -I -Psmtlib2 -olexsmtlib2.cpp smtlib2.lex Making dependencies for parsePL.cpp lexPL.cpp parseLisp.cpp lexLisp.cpp parsesmtlib.cpp lexsmtlib.cpp parsesmtlib2.cpp lexsmtlib2.cpp parser.cpp g++ -M -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -O0 -D_FORTIFY_SOURCE=2 parsePL.cpp lexPL.cpp parseLisp.cpp lexLisp.cpp parsesmtlib.cpp lexsmtlib.cpp parsesmtlib2.cpp lexsmtlib2.cpp parser.cpp >> /cvc3-2.4.1/obj/parser/x86_64-linux-gnu/Makefile.tmp g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -O0 -D_FORTIFY_SOURCE=2 -c parsePL.cpp -o '/cvc3-2.4.1/obj/parser/x86_64-linux-gnu/parsePL.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -O0 -D_FORTIFY_SOURCE=2 -c lexPL.cpp -o '/cvc3-2.4.1/obj/parser/x86_64-linux-gnu/lexPL.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -O0 -D_FORTIFY_SOURCE=2 -c parseLisp.cpp -o '/cvc3-2.4.1/obj/parser/x86_64-linux-gnu/parseLisp.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -O0 -D_FORTIFY_SOURCE=2 -c lexLisp.cpp -o '/cvc3-2.4.1/obj/parser/x86_64-linux-gnu/lexLisp.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -O0 -D_FORTIFY_SOURCE=2 -c parsesmtlib.cpp -o '/cvc3-2.4.1/obj/parser/x86_64-linux-gnu/parsesmtlib.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -O0 -D_FORTIFY_SOURCE=2 -c lexsmtlib.cpp -o '/cvc3-2.4.1/obj/parser/x86_64-linux-gnu/lexsmtlib.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -O0 -D_FORTIFY_SOURCE=2 -c parsesmtlib2.cpp -o '/cvc3-2.4.1/obj/parser/x86_64-linux-gnu/parsesmtlib2.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -O0 -D_FORTIFY_SOURCE=2 -c lexsmtlib2.cpp -o '/cvc3-2.4.1/obj/parser/x86_64-linux-gnu/lexsmtlib2.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -O0 -D_FORTIFY_SOURCE=2 -c parser.cpp -o '/cvc3-2.4.1/obj/parser/x86_64-linux-gnu/parser.o' ar ruvs '/cvc3-2.4.1/lib/x86_64-linux-gnu/libparser.a' /cvc3-2.4.1/obj/parser/x86_64-linux-gnu/parsePL.o /cvc3-2.4.1/obj/parser/x86_64-linux-gnu/lexPL.o /cvc3-2.4.1/obj/parser/x86_64-linux-gnu/parseLisp.o /cvc3-2.4.1/obj/parser/x86_64-linux-gnu/lexLisp.o /cvc3-2.4.1/obj/parser/x86_64-linux-gnu/parsesmtlib.o /cvc3-2.4.1/obj/parser/x86_64-linux-gnu/lexsmtlib.o /cvc3-2.4.1/obj/parser/x86_64-linux-gnu/parsesmtlib2.o /cvc3-2.4.1/obj/parser/x86_64-linux-gnu/lexsmtlib2.o /cvc3-2.4.1/obj/parser/x86_64-linux-gnu/parser.o ar: `u' modifier ignored since `D' is the default (see `U') ar: creating /cvc3-2.4.1/lib/x86_64-linux-gnu/libparser.a a - /cvc3-2.4.1/obj/parser/x86_64-linux-gnu/parsePL.o a - /cvc3-2.4.1/obj/parser/x86_64-linux-gnu/lexPL.o a - /cvc3-2.4.1/obj/parser/x86_64-linux-gnu/parseLisp.o a - /cvc3-2.4.1/obj/parser/x86_64-linux-gnu/lexLisp.o a - /cvc3-2.4.1/obj/parser/x86_64-linux-gnu/parsesmtlib.o a - /cvc3-2.4.1/obj/parser/x86_64-linux-gnu/lexsmtlib.o a - /cvc3-2.4.1/obj/parser/x86_64-linux-gnu/parsesmtlib2.o a - /cvc3-2.4.1/obj/parser/x86_64-linux-gnu/lexsmtlib2.o a - /cvc3-2.4.1/obj/parser/x86_64-linux-gnu/parser.o make[3]: Leaving directory '/cvc3-2.4.1/src/parser' cd translator && /usr/bin/make make[3]: Entering directory '/cvc3-2.4.1/src/translator' Making dependencies for translator.cpp g++ -M -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 translator.cpp >> /cvc3-2.4.1/obj/translator/x86_64-linux-gnu/Makefile.tmp g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c translator.cpp -o '/cvc3-2.4.1/obj/translator/x86_64-linux-gnu/translator.o' ar ruvs '/cvc3-2.4.1/lib/x86_64-linux-gnu/libtranslator.a' /cvc3-2.4.1/obj/translator/x86_64-linux-gnu/translator.o ar: `u' modifier ignored since `D' is the default (see `U') ar: creating /cvc3-2.4.1/lib/x86_64-linux-gnu/libtranslator.a a - /cvc3-2.4.1/obj/translator/x86_64-linux-gnu/translator.o make[3]: Leaving directory '/cvc3-2.4.1/src/translator' cd vcl && /usr/bin/make make[3]: Entering directory '/cvc3-2.4.1/src/vcl' Making dependencies for vcl.cpp vc_cmd.cpp g++ -M -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 vcl.cpp vc_cmd.cpp >> /cvc3-2.4.1/obj/vcl/x86_64-linux-gnu/Makefile.tmp g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c vcl.cpp -o '/cvc3-2.4.1/obj/vcl/x86_64-linux-gnu/vcl.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c vc_cmd.cpp -o '/cvc3-2.4.1/obj/vcl/x86_64-linux-gnu/vc_cmd.o' vc_cmd.cpp: In member function ‘bool CVC3::VCCmd::evaluateCommand(const CVC3::Expr&)’: vc_cmd.cpp:780:10: warning: unused variable ‘b’ [-Wunused-variable] bool b = d_vc->inconsistent(assertions); ^ ar ruvs '/cvc3-2.4.1/lib/x86_64-linux-gnu/libvcl.a' /cvc3-2.4.1/obj/vcl/x86_64-linux-gnu/vcl.o /cvc3-2.4.1/obj/vcl/x86_64-linux-gnu/vc_cmd.o ar: `u' modifier ignored since `D' is the default (see `U') ar: creating /cvc3-2.4.1/lib/x86_64-linux-gnu/libvcl.a a - /cvc3-2.4.1/obj/vcl/x86_64-linux-gnu/vcl.o a - /cvc3-2.4.1/obj/vcl/x86_64-linux-gnu/vc_cmd.o make[3]: Leaving directory '/cvc3-2.4.1/src/vcl' cd c_interface && /usr/bin/make make[3]: Entering directory '/cvc3-2.4.1/src/c_interface' Making dependencies for c_interface.cpp g++ -M -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 c_interface.cpp >> /cvc3-2.4.1/obj/c_interface/x86_64-linux-gnu/Makefile.tmp g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -D_FORTIFY_SOURCE=2 -c c_interface.cpp -o '/cvc3-2.4.1/obj/c_interface/x86_64-linux-gnu/c_interface.o' c_interface.cpp: In function ‘void* vc_bvWriteToMemoryArray(VC, Expr, Expr, Expr, int)’: c_interface.cpp:2043:9: warning: variable ‘hi’ set but not used [-Wunused-but-set-variable] int hi = newBitsPerElem - 1; ^ ar ruvs '/cvc3-2.4.1/lib/x86_64-linux-gnu/libc_interface.a' /cvc3-2.4.1/obj/c_interface/x86_64-linux-gnu/c_interface.o ar: `u' modifier ignored since `D' is the default (see `U') ar: creating /cvc3-2.4.1/lib/x86_64-linux-gnu/libc_interface.a a - /cvc3-2.4.1/obj/c_interface/x86_64-linux-gnu/c_interface.o make[3]: Leaving directory '/cvc3-2.4.1/src/c_interface' /usr/bin/make /cvc3-2.4.1/lib/libcvc3.so.5.0.0 make[3]: Entering directory '/cvc3-2.4.1/src' Building shared library /cvc3-2.4.1/lib/x86_64-linux-gnu/libcvc3.so.5.0.0 rm -rf /cvc3-2.4.1/unpack_tmp /cvc3-2.4.1/bin/unpack /cvc3-2.4.1/unpack_tmp /cvc3-2.4.1/lib/x86_64-linux-gnu/libcvc_util.a /cvc3-2.4.1/lib/x86_64-linux-gnu/libcontext.a /cvc3-2.4.1/lib/x86_64-linux-gnu/libexpr.a /cvc3-2.4.1/lib/x86_64-linux-gnu/libtheorem.a /cvc3-2.4.1/lib/x86_64-linux-gnu/libsat.a /cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_core.a /cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_arith.a /cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_array.a /cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_bitvector.a /cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_datatype.a /cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_quant.a /cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_records.a /cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_simulate.a /cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_uf.a /cvc3-2.4.1/lib/x86_64-linux-gnu/libsearch.a /cvc3-2.4.1/lib/x86_64-linux-gnu/libparser.a /cvc3-2.4.1/lib/x86_64-linux-gnu/libtranslator.a /cvc3-2.4.1/lib/x86_64-linux-gnu/libvcl.a /cvc3-2.4.1/lib/x86_64-linux-gnu/libc_interface.a > UNPACKED Found 86 members in 19 libraries Unpacking cvc_util Unpacking context Unpacking expr Unpacking theorem Unpacking sat Unpacking theory_core Unpacking theory_arith Unpacking theory_array Unpacking theory_bitvector Unpacking theory_datatype Unpacking theory_quant Unpacking theory_records Unpacking theory_simulate Unpacking theory_uf Unpacking search Unpacking parser Unpacking translator Unpacking vcl Unpacking c_interface cat UNPACKED | xargs g++ -shared -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -Wl,-z,relro \ -Wl,-soname,libcvc3.so.5 -o '/cvc3-2.4.1/lib/x86_64-linux-gnu/libcvc3.so.5.0.0' `` -lgmp /sbin/ldconfig -nv /cvc3-2.4.1/lib/x86_64-linux-gnu /cvc3-2.4.1/lib/x86_64-linux-gnu: libcvc3.so.5 -> libcvc3.so.5.0.0 (changed) ln -sf libcvc3.so.5.0.0 /cvc3-2.4.1/lib/x86_64-linux-gnu/libcvc3.so.5.0 ln -sf libcvc3.so.5.0.0 /cvc3-2.4.1/lib/x86_64-linux-gnu/libcvc3.so.5 ln -sf libcvc3.so.5.0.0 /cvc3-2.4.1/lib/x86_64-linux-gnu/libcvc3.so ln -sf /cvc3-2.4.1/lib/x86_64-linux-gnu/libcvc3.so.5.0.0 '/cvc3-2.4.1/lib//libcvc3.so.5.0.0' /sbin/ldconfig -nv '/cvc3-2.4.1/lib/' /cvc3-2.4.1/lib: libcvc3.so.5 -> libcvc3.so.5.0.0 (changed) ln -sf libcvc3.so.5.0.0 '/cvc3-2.4.1/lib//libcvc3.so.5.0' ln -sf libcvc3.so.5.0.0 '/cvc3-2.4.1/lib//libcvc3.so.5' ln -sf libcvc3.so.5.0.0 '/cvc3-2.4.1/lib//libcvc3.so' make[3]: Leaving directory '/cvc3-2.4.1/src' cd cvc3 && /usr/bin/make VERSION=2.4.1 make[3]: Entering directory '/cvc3-2.4.1/src/cvc3' Making dependencies for main.cpp g++ -M -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -DVERSION=\"2.4.1\" -D_FORTIFY_SOURCE=2 main.cpp >> /cvc3-2.4.1/obj/cvc3/x86_64-linux-gnu/Makefile.tmp /usr/bin/make /cvc3-2.4.1/bin/x86_64-linux-gnu/cvc3 make[4]: Entering directory '/cvc3-2.4.1/src/cvc3' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -DVERSION=\"2.4.1\" -D_FORTIFY_SOURCE=2 -c main.cpp -o '/cvc3-2.4.1/obj/cvc3/x86_64-linux-gnu/main.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -DVERSION=\"2.4.1\" -Wl,-z,relro -o '/cvc3-2.4.1/bin/x86_64-linux-gnu/cvc3' /cvc3-2.4.1/obj/cvc3/x86_64-linux-gnu/main.o \ -L/cvc3-2.4.1/lib/x86_64-linux-gnu -lcvc3 -lgmp make[4]: Leaving directory '/cvc3-2.4.1/src/cvc3' ln -sf /cvc3-2.4.1/bin/x86_64-linux-gnu/cvc3 /cvc3-2.4.1/bin/cvc3 make[3]: Leaving directory '/cvc3-2.4.1/src/cvc3' make[2]: Leaving directory '/cvc3-2.4.1/src' cd /cvc3-2.4.1/java; /usr/bin/make VERSION=2.4.1 make[2]: Entering directory '/cvc3-2.4.1/java' if [ ! -d obj ]; then mkdir -p obj; fi /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/JniUtils.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/Cvc3Exception.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/TypecheckException.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/SoundException.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/EvalException.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/CLException.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/ParserException.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/SmtlibException.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/DebugException.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/Embedded.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/EmbeddedManager.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/InputLanguage.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/QueryResult.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/SatResult.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/FormulaValue.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/Expr.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/ExprMut.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/ExprManager.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/ExprManagerMut.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/Type.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/TypeMut.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/Op.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/OpMut.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/Rational.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/RationalMut.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/Theorem.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/TheoremMut.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/Proof.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/ProofMut.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/Context.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/ContextMut.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/Flag.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/Flags.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/FlagsMut.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/Statistics.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/StatisticsMut.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/ValidityChecker.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/Test.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/TimeoutHandler.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javac -Xlint -g -source 1.4 -sourcepath src \ -d obj src/cvc3/Cvc3.java warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. 4 warnings /usr/lib/jvm/default-java/bin/javah -jni -force -classpath obj \ -o include/cvc3/EmbeddedManager.h cvc3.EmbeddedManager /usr/lib/jvm/default-java/bin/javah -jni -force -classpath obj \ -o include/cvc3/Expr.h cvc3.Expr /usr/lib/jvm/default-java/bin/javah -jni -force -classpath obj \ -o include/cvc3/ExprMut.h cvc3.ExprMut /usr/lib/jvm/default-java/bin/javah -jni -force -classpath obj \ -o include/cvc3/ExprManager.h cvc3.ExprManager /usr/lib/jvm/default-java/bin/javah -jni -force -classpath obj \ -o include/cvc3/Type.h cvc3.Type /usr/lib/jvm/default-java/bin/javah -jni -force -classpath obj \ -o include/cvc3/TypeMut.h cvc3.TypeMut /usr/lib/jvm/default-java/bin/javah -jni -force -classpath obj \ -o include/cvc3/Op.h cvc3.Op /usr/lib/jvm/default-java/bin/javah -jni -force -classpath obj \ -o include/cvc3/OpMut.h cvc3.OpMut /usr/lib/jvm/default-java/bin/javah -jni -force -classpath obj \ -o include/cvc3/Rational.h cvc3.Rational /usr/lib/jvm/default-java/bin/javah -jni -force -classpath obj \ -o include/cvc3/RationalMut.h cvc3.RationalMut /usr/lib/jvm/default-java/bin/javah -jni -force -classpath obj \ -o include/cvc3/Theorem.h cvc3.Theorem /usr/lib/jvm/default-java/bin/javah -jni -force -classpath obj \ -o include/cvc3/TheoremMut.h cvc3.TheoremMut /usr/lib/jvm/default-java/bin/javah -jni -force -classpath obj \ -o include/cvc3/Proof.h cvc3.Proof /usr/lib/jvm/default-java/bin/javah -jni -force -classpath obj \ -o include/cvc3/ProofMut.h cvc3.ProofMut /usr/lib/jvm/default-java/bin/javah -jni -force -classpath obj \ -o include/cvc3/Context.h cvc3.Context /usr/lib/jvm/default-java/bin/javah -jni -force -classpath obj \ -o include/cvc3/ContextMut.h cvc3.ContextMut /usr/lib/jvm/default-java/bin/javah -jni -force -classpath obj \ -o include/cvc3/Flag.h cvc3.Flag /usr/lib/jvm/default-java/bin/javah -jni -force -classpath obj \ -o include/cvc3/Flags.h cvc3.Flags /usr/lib/jvm/default-java/bin/javah -jni -force -classpath obj \ -o include/cvc3/FlagsMut.h cvc3.FlagsMut /usr/lib/jvm/default-java/bin/javah -jni -force -classpath obj \ -o include/cvc3/Statistics.h cvc3.Statistics /usr/lib/jvm/default-java/bin/javah -jni -force -classpath obj \ -o include/cvc3/StatisticsMut.h cvc3.StatisticsMut /usr/lib/jvm/default-java/bin/javah -jni -force -classpath obj \ -o include/cvc3/ValidityChecker.h cvc3.ValidityChecker g++ -D_FORTIFY_SOURCE=2 -I/usr/lib/jvm/default-java/include -I/usr/lib/jvm/default-java/include/linux -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -c \ -I ../src/include -I include/cvc3/ \ -o obj/cvc3/JniUtils.o src/cvc3/JniUtils.cpp src/cvc3/JniUtils.cpp: In function ‘_jstring* Java_cvc3_JniUtils::toJava(JNIEnv*, CVC3::InputLanguage)’: src/cvc3/JniUtils.cpp:73:12: warning: enumeration value ‘AST_LANG’ not handled in switch [-Wswitch] switch (lang) { ^ src/cvc3/JniUtils.cpp:73:12: warning: enumeration value ‘SIMPLIFY_LANG’ not handled in switch [-Wswitch] src/cvc3/JniUtils.cpp:73:12: warning: enumeration value ‘TPTP_LANG’ not handled in switch [-Wswitch] src/cvc3/JniUtils.cpp:73:12: warning: enumeration value ‘SPASS_LANG’ not handled in switch [-Wswitch] src/cvc3/JniUtils.cpp:73:12: warning: enumeration value ‘SMTLIB_V2_LANG’ not handled in switch [-Wswitch] src/cvc3/JniUtils.cpp: In function ‘_jobjectArray* Java_cvc3_JniUtils::toJavaV(JNIEnv*, const std::vector >&)’: src/cvc3/JniUtils.cpp:159:22: warning: comparison between signed and unsigned integer expressions [-Wsign-compare] for(int i = 0; i < v.size(); ++i) { ^ src/cvc3/JniUtils.cpp: In function ‘_jstring* Java_cvc3_JniUtils::toJava(JNIEnv*, CVC3::QueryResult)’: src/cvc3/JniUtils.cpp:60:3: warning: control reaches end of non-void function [-Wreturn-type] } ^ src/cvc3/JniUtils.cpp: In function ‘_jstring* Java_cvc3_JniUtils::toJava(JNIEnv*, CVC3::FormulaValue)’: src/cvc3/JniUtils.cpp:70:3: warning: control reaches end of non-void function [-Wreturn-type] } ^ src/cvc3/JniUtils.cpp: In function ‘_jstring* Java_cvc3_JniUtils::toJava(JNIEnv*, CVC3::InputLanguage)’: src/cvc3/JniUtils.cpp:80:3: warning: control reaches end of non-void function [-Wreturn-type] } ^ src/cvc3/JniUtils.cpp: In function ‘CVC3::InputLanguage Java_cvc3_JniUtils::toCppInputLanguage(JNIEnv*, const string&)’: src/cvc3/JniUtils.cpp:92:3: warning: control reaches end of non-void function [-Wreturn-type] } ^ /usr/bin/python ./create_impl.py \ include/cvc3/EmbeddedManager.h \ src/cvc3/EmbeddedManager_impl.cpp \ src/cvc3/EmbeddedManager.cpp g++ -D_FORTIFY_SOURCE=2 -I/usr/lib/jvm/default-java/include -I/usr/lib/jvm/default-java/include/linux -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -c \ -I ../src/include -I include/cvc3/ \ -o obj/cvc3/EmbeddedManager.o src/cvc3/EmbeddedManager.cpp /usr/bin/python ./create_impl.py \ include/cvc3/Expr.h \ src/cvc3/Expr_impl.cpp \ src/cvc3/Expr.cpp g++ -D_FORTIFY_SOURCE=2 -I/usr/lib/jvm/default-java/include -I/usr/lib/jvm/default-java/include/linux -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -c \ -I ../src/include -I include/cvc3/ \ -o obj/cvc3/Expr.o src/cvc3/Expr.cpp src/cvc3/Expr.cpp: In function ‘_jobject* Java_cvc3_Expr_jniGetKid(JNIEnv*, jclass, jobject, jint)’: src/cvc3/Expr.cpp:903:9: warning: unused variable ‘i’ [-Wunused-variable] int i(ji); ^ In file included from src/cvc3/Expr.cpp:5:0: include/cvc3/JniUtils.h: In instantiation of ‘_jobjectArray* Java_cvc3_JniUtils::toJavaVConstRef(JNIEnv*, const std::vector&) [with T = CVC3::Expr; jobjectArray = _jobjectArray*; JNIEnv = JNIEnv_]’: src/cvc3/Expr.cpp:734:48: required from here include/cvc3/JniUtils.h:185:23: warning: comparison between signed and unsigned integer expressions [-Wsign-compare] for (int i = 0; i < v.size(); ++i) { ^ include/cvc3/JniUtils.h: In instantiation of ‘_jobjectArray* Java_cvc3_JniUtils::toJavaVVConstRef(JNIEnv*, const std::vector >&) [with T = CVC3::Expr; jobjectArray = _jobjectArray*; JNIEnv = JNIEnv_]’: src/cvc3/Expr.cpp:799:53: required from here include/cvc3/JniUtils.h:198:25: warning: comparison between signed and unsigned integer expressions [-Wsign-compare] for (int i = 0; i < v.size(); ++i) ^ /usr/bin/python ./create_impl.py \ include/cvc3/ExprMut.h \ src/cvc3/ExprMut_impl.cpp \ src/cvc3/ExprMut.cpp g++ -D_FORTIFY_SOURCE=2 -I/usr/lib/jvm/default-java/include -I/usr/lib/jvm/default-java/include/linux -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -c \ -I ../src/include -I include/cvc3/ \ -o obj/cvc3/ExprMut.o src/cvc3/ExprMut.cpp /usr/bin/python ./create_impl.py \ include/cvc3/ExprManager.h \ src/cvc3/ExprManager_impl.cpp \ src/cvc3/ExprManager.cpp g++ -D_FORTIFY_SOURCE=2 -I/usr/lib/jvm/default-java/include -I/usr/lib/jvm/default-java/include/linux -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -c \ -I ../src/include -I include/cvc3/ \ -o obj/cvc3/ExprManager.o src/cvc3/ExprManager.cpp /usr/bin/python ./create_impl.py \ include/cvc3/Type.h \ src/cvc3/Type_impl.cpp \ src/cvc3/Type.cpp g++ -D_FORTIFY_SOURCE=2 -I/usr/lib/jvm/default-java/include -I/usr/lib/jvm/default-java/include/linux -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -c \ -I ../src/include -I include/cvc3/ \ -o obj/cvc3/Type.o src/cvc3/Type.cpp /usr/bin/python ./create_impl.py \ include/cvc3/TypeMut.h \ src/cvc3/TypeMut_impl.cpp \ src/cvc3/TypeMut.cpp g++ -D_FORTIFY_SOURCE=2 -I/usr/lib/jvm/default-java/include -I/usr/lib/jvm/default-java/include/linux -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -c \ -I ../src/include -I include/cvc3/ \ -o obj/cvc3/TypeMut.o src/cvc3/TypeMut.cpp /usr/bin/python ./create_impl.py \ include/cvc3/Op.h \ src/cvc3/Op_impl.cpp \ src/cvc3/Op.cpp g++ -D_FORTIFY_SOURCE=2 -I/usr/lib/jvm/default-java/include -I/usr/lib/jvm/default-java/include/linux -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -c \ -I ../src/include -I include/cvc3/ \ -o obj/cvc3/Op.o src/cvc3/Op.cpp /usr/bin/python ./create_impl.py \ include/cvc3/OpMut.h \ src/cvc3/OpMut_impl.cpp \ src/cvc3/OpMut.cpp g++ -D_FORTIFY_SOURCE=2 -I/usr/lib/jvm/default-java/include -I/usr/lib/jvm/default-java/include/linux -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -c \ -I ../src/include -I include/cvc3/ \ -o obj/cvc3/OpMut.o src/cvc3/OpMut.cpp /usr/bin/python ./create_impl.py \ include/cvc3/Rational.h \ src/cvc3/Rational_impl.cpp \ src/cvc3/Rational.cpp g++ -D_FORTIFY_SOURCE=2 -I/usr/lib/jvm/default-java/include -I/usr/lib/jvm/default-java/include/linux -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -c \ -I ../src/include -I include/cvc3/ \ -o obj/cvc3/Rational.o src/cvc3/Rational.cpp /usr/bin/python ./create_impl.py \ include/cvc3/RationalMut.h \ src/cvc3/RationalMut_impl.cpp \ src/cvc3/RationalMut.cpp g++ -D_FORTIFY_SOURCE=2 -I/usr/lib/jvm/default-java/include -I/usr/lib/jvm/default-java/include/linux -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -c \ -I ../src/include -I include/cvc3/ \ -o obj/cvc3/RationalMut.o src/cvc3/RationalMut.cpp /usr/bin/python ./create_impl.py \ include/cvc3/Theorem.h \ src/cvc3/Theorem_impl.cpp \ src/cvc3/Theorem.cpp g++ -D_FORTIFY_SOURCE=2 -I/usr/lib/jvm/default-java/include -I/usr/lib/jvm/default-java/include/linux -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -c \ -I ../src/include -I include/cvc3/ \ -o obj/cvc3/Theorem.o src/cvc3/Theorem.cpp /usr/bin/python ./create_impl.py \ include/cvc3/TheoremMut.h \ src/cvc3/TheoremMut_impl.cpp \ src/cvc3/TheoremMut.cpp g++ -D_FORTIFY_SOURCE=2 -I/usr/lib/jvm/default-java/include -I/usr/lib/jvm/default-java/include/linux -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -c \ -I ../src/include -I include/cvc3/ \ -o obj/cvc3/TheoremMut.o src/cvc3/TheoremMut.cpp /usr/bin/python ./create_impl.py \ include/cvc3/Proof.h \ src/cvc3/Proof_impl.cpp \ src/cvc3/Proof.cpp g++ -D_FORTIFY_SOURCE=2 -I/usr/lib/jvm/default-java/include -I/usr/lib/jvm/default-java/include/linux -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -c \ -I ../src/include -I include/cvc3/ \ -o obj/cvc3/Proof.o src/cvc3/Proof.cpp /usr/bin/python ./create_impl.py \ include/cvc3/ProofMut.h \ src/cvc3/ProofMut_impl.cpp \ src/cvc3/ProofMut.cpp g++ -D_FORTIFY_SOURCE=2 -I/usr/lib/jvm/default-java/include -I/usr/lib/jvm/default-java/include/linux -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -c \ -I ../src/include -I include/cvc3/ \ -o obj/cvc3/ProofMut.o src/cvc3/ProofMut.cpp /usr/bin/python ./create_impl.py \ include/cvc3/Context.h \ src/cvc3/Context_impl.cpp \ src/cvc3/Context.cpp g++ -D_FORTIFY_SOURCE=2 -I/usr/lib/jvm/default-java/include -I/usr/lib/jvm/default-java/include/linux -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -c \ -I ../src/include -I include/cvc3/ \ -o obj/cvc3/Context.o src/cvc3/Context.cpp /usr/bin/python ./create_impl.py \ include/cvc3/ContextMut.h \ src/cvc3/ContextMut_impl.cpp \ src/cvc3/ContextMut.cpp g++ -D_FORTIFY_SOURCE=2 -I/usr/lib/jvm/default-java/include -I/usr/lib/jvm/default-java/include/linux -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -c \ -I ../src/include -I include/cvc3/ \ -o obj/cvc3/ContextMut.o src/cvc3/ContextMut.cpp /usr/bin/python ./create_impl.py \ include/cvc3/Flag.h \ src/cvc3/Flag_impl.cpp \ src/cvc3/Flag.cpp g++ -D_FORTIFY_SOURCE=2 -I/usr/lib/jvm/default-java/include -I/usr/lib/jvm/default-java/include/linux -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -c \ -I ../src/include -I include/cvc3/ \ -o obj/cvc3/Flag.o src/cvc3/Flag.cpp /usr/bin/python ./create_impl.py \ include/cvc3/Flags.h \ src/cvc3/Flags_impl.cpp \ src/cvc3/Flags.cpp g++ -D_FORTIFY_SOURCE=2 -I/usr/lib/jvm/default-java/include -I/usr/lib/jvm/default-java/include/linux -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -c \ -I ../src/include -I include/cvc3/ \ -o obj/cvc3/Flags.o src/cvc3/Flags.cpp /usr/bin/python ./create_impl.py \ include/cvc3/FlagsMut.h \ src/cvc3/FlagsMut_impl.cpp \ src/cvc3/FlagsMut.cpp g++ -D_FORTIFY_SOURCE=2 -I/usr/lib/jvm/default-java/include -I/usr/lib/jvm/default-java/include/linux -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -c \ -I ../src/include -I include/cvc3/ \ -o obj/cvc3/FlagsMut.o src/cvc3/FlagsMut.cpp /usr/bin/python ./create_impl.py \ include/cvc3/Statistics.h \ src/cvc3/Statistics_impl.cpp \ src/cvc3/Statistics.cpp g++ -D_FORTIFY_SOURCE=2 -I/usr/lib/jvm/default-java/include -I/usr/lib/jvm/default-java/include/linux -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -c \ -I ../src/include -I include/cvc3/ \ -o obj/cvc3/Statistics.o src/cvc3/Statistics.cpp /usr/bin/python ./create_impl.py \ include/cvc3/StatisticsMut.h \ src/cvc3/StatisticsMut_impl.cpp \ src/cvc3/StatisticsMut.cpp g++ -D_FORTIFY_SOURCE=2 -I/usr/lib/jvm/default-java/include -I/usr/lib/jvm/default-java/include/linux -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -c \ -I ../src/include -I include/cvc3/ \ -o obj/cvc3/StatisticsMut.o src/cvc3/StatisticsMut.cpp /usr/bin/python ./create_impl.py \ include/cvc3/ValidityChecker.h \ src/cvc3/ValidityChecker_impl.cpp \ src/cvc3/ValidityChecker.cpp g++ -D_FORTIFY_SOURCE=2 -I/usr/lib/jvm/default-java/include -I/usr/lib/jvm/default-java/include/linux -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -c \ -I ../src/include -I include/cvc3/ \ -o obj/cvc3/ValidityChecker.o src/cvc3/ValidityChecker.cpp src/cvc3/ValidityChecker.cpp: In function ‘_jobject* Java_cvc3_ValidityChecker_jniArrayLiteral(JNIEnv*, jclass, jobject, jobject, jobject)’: src/cvc3/ValidityChecker.cpp:311:22: warning: unused variable ‘vc’ [-Wunused-variable] ValidityChecker* vc = unembed_mut(env, jvc); ^ src/cvc3/ValidityChecker.cpp: In function ‘_jobject* Java_cvc3_ValidityChecker_jniNullExpr(JNIEnv*, jclass, jobject)’: src/cvc3/ValidityChecker.cpp:441:22: warning: unused variable ‘vc’ [-Wunused-variable] ValidityChecker* vc = unembed_mut(env, jvc); ^ src/cvc3/ValidityChecker.cpp: In function ‘_jobject* Java_cvc3_ValidityChecker_jniRecordExpr3(JNIEnv*, jclass, jobject, jstring, jobject, jstring, jobject, jstring, jobject)’: src/cvc3/ValidityChecker.cpp:1460:17: warning: unused variable ‘expr3’ [-Wunused-variable] const Expr* expr3 = unembed_const(env, jexpr3); ^ src/cvc3/ValidityChecker.cpp: In function ‘_jobject* Java_cvc3_ValidityChecker_jniNewBVConstExpr1(JNIEnv*, jclass, jobject, jstring, jint)’: src/cvc3/ValidityChecker.cpp:1552:9: warning: unused variable ‘base’ [-Wunused-variable] int base(jbase); ^ In file included from src/cvc3/ValidityChecker.cpp:4:0: include/cvc3/JniUtils.h: In instantiation of ‘_jobjectArray* Java_cvc3_JniUtils::toJavaVCopy(JNIEnv*, const std::vector&) [with T = CVC3::Type; jobjectArray = _jobjectArray*; JNIEnv = JNIEnv_]’: src/cvc3/ValidityChecker.cpp:286:35: required from here include/cvc3/JniUtils.h:171:23: warning: comparison between signed and unsigned integer expressions [-Wsign-compare] for (int i = 0; i < v.size(); ++i) { ^ include/cvc3/JniUtils.h: In instantiation of ‘_jobjectArray* Java_cvc3_JniUtils::toJavaVCopy(JNIEnv*, const std::vector&) [with T = CVC3::Expr; jobjectArray = _jobjectArray*; JNIEnv = JNIEnv_]’: src/cvc3/ValidityChecker.cpp:2519:35: required from here include/cvc3/JniUtils.h:171:23: warning: comparison between signed and unsigned integer expressions [-Wsign-compare] include/cvc3/JniUtils.h: In instantiation of ‘_jobjectArray* Java_cvc3_JniUtils::toJavaVCopy(JNIEnv*, const std::vector&) [with T = std::__cxx11::basic_string; jobjectArray = _jobjectArray*; JNIEnv = JNIEnv_]’: src/cvc3/ValidityChecker.cpp:2667:35: required from here include/cvc3/JniUtils.h:171:23: warning: comparison between signed and unsigned integer expressions [-Wsign-compare] if [ ! -d /cvc3-2.4.1/java/lib/x86_64-linux-gnu ]; then mkdir -p /cvc3-2.4.1/java/lib/x86_64-linux-gnu; fi g++ -shared -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wl,-z,relro \ -Wl,-soname,libcvc3jni.so.5.0 \ -L ../lib obj/cvc3/*.o \ -o /cvc3-2.4.1/java/lib/x86_64-linux-gnu/libcvc3jni.so.5.0.0 -lcvc3 -lgmp /sbin/ldconfig -nv /cvc3-2.4.1/java/lib/x86_64-linux-gnu /cvc3-2.4.1/java/lib/x86_64-linux-gnu: libcvc3jni.so.5.0 -> libcvc3jni.so.5.0.0 (changed) ln -sf libcvc3jni.so.5.0.0 /cvc3-2.4.1/java/lib/x86_64-linux-gnu/libcvc3jni.so.5.0 ln -sf libcvc3jni.so.5.0.0 /cvc3-2.4.1/java/lib/x86_64-linux-gnu/libcvc3jni.so.5 ln -sf libcvc3jni.so.5.0.0 /cvc3-2.4.1/java/lib/x86_64-linux-gnu/libcvc3jni.so ln -sf /cvc3-2.4.1/java/lib/x86_64-linux-gnu/libcvc3jni.so.5.0.0 /cvc3-2.4.1/java/lib/libcvc3jni.so.5.0.0 ln -sf libcvc3jni.so.5.0.0 '/cvc3-2.4.1/java/lib//libcvc3jni.so.5.0' ln -sf libcvc3jni.so.5.0.0 '/cvc3-2.4.1/java/lib//libcvc3jni.so.5' ln -sf libcvc3jni.so.5.0.0 '/cvc3-2.4.1/java/lib//libcvc3jni.so' if [ ! -d /cvc3-2.4.1/java/lib ]; then mkdir -p /cvc3-2.4.1/java/lib; fi cd obj && /usr/lib/jvm/default-java/bin/jar cf ../../java/lib/libcvc3-5.0.0.jar cvc3/*.class echo -e "Main-Class: cvc3/Test\nClass-Path: libcvc3-5.0.0.jar\n" > Test_manifest /usr/lib/jvm/default-java/bin/jar -cmf Test_manifest ../java/lib/cvc3test.jar /usr/lib/jvm/default-java/bin/jar -uf ../java/lib/cvc3test.jar -C obj cvc3/Test.class /usr/lib/jvm/default-java/bin/jar -cmf Cvc3_manifest ../java/lib/cvc3.jar /usr/lib/jvm/default-java/bin/jar -uf ../java/lib/cvc3.jar -C obj cvc3/TimeoutHandler.class /usr/lib/jvm/default-java/bin/jar -uf ../java/lib/cvc3.jar -C obj cvc3/Cvc3.class make[2]: Leaving directory '/cvc3-2.4.1/java' find /cvc3-2.4.1/src '(' -name "*.h" -o -name "*.cpp" -o \ -name "*.y" ')' \ ! -name "lexPL.cpp" ! -name "parsePL.cpp" \ -print > FILES make[1]: Leaving directory '/cvc3-2.4.1' touch debian/stamp-makefile-build /usr/bin/make -C . regress0 LD_LIBRARY_PATH=/cvc3-2.4.1/lib make[1]: Entering directory '/cvc3-2.4.1' /usr/bin/make regress REGRESS_LEVEL=0 make[2]: Entering directory '/cvc3-2.4.1' cd /cvc3-2.4.1/src; /usr/bin/make VERSION=2.4.1 make[3]: Entering directory '/cvc3-2.4.1/src' cd util && /usr/bin/make make[4]: Entering directory '/cvc3-2.4.1/src/util' make[4]: Nothing to be done for 'all'. make[4]: Leaving directory '/cvc3-2.4.1/src/util' cd context && /usr/bin/make make[4]: Entering directory '/cvc3-2.4.1/src/context' make[4]: Nothing to be done for 'all'. make[4]: Leaving directory '/cvc3-2.4.1/src/context' cd expr && /usr/bin/make make[4]: Entering directory '/cvc3-2.4.1/src/expr' make[4]: Nothing to be done for 'all'. make[4]: Leaving directory '/cvc3-2.4.1/src/expr' cd theorem && /usr/bin/make make[4]: Entering directory '/cvc3-2.4.1/src/theorem' make[4]: Nothing to be done for 'all'. make[4]: Leaving directory '/cvc3-2.4.1/src/theorem' cd sat && /usr/bin/make make[4]: Entering directory '/cvc3-2.4.1/src/sat' make[4]: Nothing to be done for 'all'. make[4]: Leaving directory '/cvc3-2.4.1/src/sat' cd theory_core && /usr/bin/make make[4]: Entering directory '/cvc3-2.4.1/src/theory_core' make[4]: Nothing to be done for 'all'. make[4]: Leaving directory '/cvc3-2.4.1/src/theory_core' cd theory_arith && /usr/bin/make make[4]: Entering directory '/cvc3-2.4.1/src/theory_arith' make[4]: Nothing to be done for 'all'. make[4]: Leaving directory '/cvc3-2.4.1/src/theory_arith' cd theory_array && /usr/bin/make make[4]: Entering directory '/cvc3-2.4.1/src/theory_array' make[4]: Nothing to be done for 'all'. make[4]: Leaving directory '/cvc3-2.4.1/src/theory_array' cd theory_bitvector && /usr/bin/make make[4]: Entering directory '/cvc3-2.4.1/src/theory_bitvector' make[4]: Nothing to be done for 'all'. make[4]: Leaving directory '/cvc3-2.4.1/src/theory_bitvector' cd theory_datatype && /usr/bin/make make[4]: Entering directory '/cvc3-2.4.1/src/theory_datatype' make[4]: Nothing to be done for 'all'. make[4]: Leaving directory '/cvc3-2.4.1/src/theory_datatype' cd theory_quant && /usr/bin/make make[4]: Entering directory '/cvc3-2.4.1/src/theory_quant' make[4]: Nothing to be done for 'all'. make[4]: Leaving directory '/cvc3-2.4.1/src/theory_quant' cd theory_records && /usr/bin/make make[4]: Entering directory '/cvc3-2.4.1/src/theory_records' make[4]: Nothing to be done for 'all'. make[4]: Leaving directory '/cvc3-2.4.1/src/theory_records' cd theory_simulate && /usr/bin/make make[4]: Entering directory '/cvc3-2.4.1/src/theory_simulate' make[4]: Nothing to be done for 'all'. make[4]: Leaving directory '/cvc3-2.4.1/src/theory_simulate' cd theory_uf && /usr/bin/make make[4]: Entering directory '/cvc3-2.4.1/src/theory_uf' make[4]: Nothing to be done for 'all'. make[4]: Leaving directory '/cvc3-2.4.1/src/theory_uf' cd search && /usr/bin/make make[4]: Entering directory '/cvc3-2.4.1/src/search' make[4]: Nothing to be done for 'all'. make[4]: Leaving directory '/cvc3-2.4.1/src/search' cd parser && /usr/bin/make make[4]: Entering directory '/cvc3-2.4.1/src/parser' make[4]: Nothing to be done for 'all'. make[4]: Leaving directory '/cvc3-2.4.1/src/parser' cd translator && /usr/bin/make make[4]: Entering directory '/cvc3-2.4.1/src/translator' make[4]: Nothing to be done for 'all'. make[4]: Leaving directory '/cvc3-2.4.1/src/translator' cd vcl && /usr/bin/make make[4]: Entering directory '/cvc3-2.4.1/src/vcl' make[4]: Nothing to be done for 'all'. make[4]: Leaving directory '/cvc3-2.4.1/src/vcl' cd c_interface && /usr/bin/make make[4]: Entering directory '/cvc3-2.4.1/src/c_interface' make[4]: Nothing to be done for 'all'. make[4]: Leaving directory '/cvc3-2.4.1/src/c_interface' /usr/bin/make /cvc3-2.4.1/lib/libcvc3.so.5.0.0 make[4]: Entering directory '/cvc3-2.4.1/src' ln -sf /cvc3-2.4.1/lib/x86_64-linux-gnu/libcvc3.so.5.0.0 '/cvc3-2.4.1/lib//libcvc3.so.5.0.0' /sbin/ldconfig -nv '/cvc3-2.4.1/lib/' /cvc3-2.4.1/lib: libcvc3.so.5 -> libcvc3.so.5.0.0 ln -sf libcvc3.so.5.0.0 '/cvc3-2.4.1/lib//libcvc3.so.5.0' ln -sf libcvc3.so.5.0.0 '/cvc3-2.4.1/lib//libcvc3.so.5' ln -sf libcvc3.so.5.0.0 '/cvc3-2.4.1/lib//libcvc3.so' make[4]: Leaving directory '/cvc3-2.4.1/src' cd cvc3 && /usr/bin/make VERSION=2.4.1 make[4]: Entering directory '/cvc3-2.4.1/src/cvc3' /usr/bin/make /cvc3-2.4.1/bin/x86_64-linux-gnu/cvc3 make[5]: Entering directory '/cvc3-2.4.1/src/cvc3' make[5]: '/cvc3-2.4.1/bin/x86_64-linux-gnu/cvc3' is up to date. make[5]: Leaving directory '/cvc3-2.4.1/src/cvc3' ln -sf /cvc3-2.4.1/bin/x86_64-linux-gnu/cvc3 /cvc3-2.4.1/bin/cvc3 make[4]: Leaving directory '/cvc3-2.4.1/src/cvc3' make[3]: Leaving directory '/cvc3-2.4.1/src' cd /cvc3-2.4.1/java; /usr/bin/make VERSION=2.4.1 make[3]: Entering directory '/cvc3-2.4.1/java' if [ ! -d obj ]; then mkdir -p obj; fi if [ ! -d /cvc3-2.4.1/java/lib/x86_64-linux-gnu ]; then mkdir -p /cvc3-2.4.1/java/lib/x86_64-linux-gnu; fi g++ -shared -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wl,-z,relro \ -Wl,-soname,libcvc3jni.so.5.0 \ -L ../lib obj/cvc3/*.o \ -o /cvc3-2.4.1/java/lib/x86_64-linux-gnu/libcvc3jni.so.5.0.0 -lcvc3 -lgmp /sbin/ldconfig -nv /cvc3-2.4.1/java/lib/x86_64-linux-gnu /cvc3-2.4.1/java/lib/x86_64-linux-gnu: libcvc3jni.so.5.0 -> libcvc3jni.so.5.0.0 ln -sf libcvc3jni.so.5.0.0 /cvc3-2.4.1/java/lib/x86_64-linux-gnu/libcvc3jni.so.5.0 ln -sf libcvc3jni.so.5.0.0 /cvc3-2.4.1/java/lib/x86_64-linux-gnu/libcvc3jni.so.5 ln -sf libcvc3jni.so.5.0.0 /cvc3-2.4.1/java/lib/x86_64-linux-gnu/libcvc3jni.so if [ ! -d /cvc3-2.4.1/java/lib ]; then mkdir -p /cvc3-2.4.1/java/lib; fi make[3]: Leaving directory '/cvc3-2.4.1/java' find /cvc3-2.4.1/src '(' -name "*.h" -o -name "*.cpp" -o \ -name "*.y" ')' \ ! -name "lexPL.cpp" ! -name "parsePL.cpp" \ -print > FILES cd /cvc3-2.4.1/test; /usr/bin/make make[3]: Entering directory '/cvc3-2.4.1/test' Making dependencies for main.cpp george.cpp g++ -M -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -O0 -D_FORTIFY_SOURCE=2 main.cpp george.cpp >> /cvc3-2.4.1/test/obj/x86_64-linux-gnu/Makefile.tmp /usr/bin/make /cvc3-2.4.1/test/bin/x86_64-linux-gnu/test make[4]: Entering directory '/cvc3-2.4.1/test' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -O0 -D_FORTIFY_SOURCE=2 -c main.cpp -o '/cvc3-2.4.1/test/obj/x86_64-linux-gnu/main.o' main.cpp: In function ‘bool check(CVC3::ValidityChecker*, CVC3::Expr, bool)’: main.cpp:39:14: warning: switch condition has type bool [-Wswitch-bool] switch (res) { ^ main.cpp: In function ‘void test11()’: main.cpp:1024:18: warning: variable ‘c’ set but not used [-Wunused-but-set-variable] unsigned int c; ^ main.cpp: In function ‘void test18()’: main.cpp:1642:10: warning: variable ‘b’ set but not used [-Wunused-but-set-variable] bool b = check(vc, vc->impliesExpr(vc->datatypeTestExpr("succ", x), spxeqx)); ^ main.cpp: In function ‘void test26()’: main.cpp:2042:10: warning: variable ‘b’ set but not used [-Wunused-but-set-variable] bool b = check(vc, vc->eqExpr(e1, e2)); ^ g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -O0 -D_FORTIFY_SOURCE=2 -c george.cpp -o '/cvc3-2.4.1/test/obj/x86_64-linux-gnu/george.o' g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -O0 -Wl,-z,relro -o '/cvc3-2.4.1/test/bin/x86_64-linux-gnu/test' /cvc3-2.4.1/test/obj/x86_64-linux-gnu/main.o /cvc3-2.4.1/test/obj/x86_64-linux-gnu/george.o \ -L/cvc3-2.4.1/lib/x86_64-linux-gnu -lcvc3 -lgmp make[4]: Leaving directory '/cvc3-2.4.1/test' ln -sf /cvc3-2.4.1/test/bin/x86_64-linux-gnu/test /cvc3-2.4.1/test/bin/test make[3]: Leaving directory '/cvc3-2.4.1/test' cd /cvc3-2.4.1/testc; /usr/bin/make make[3]: Entering directory '/cvc3-2.4.1/testc' Making dependencies for gcc -M -g -I../src/include main.c >> /cvc3-2.4.1/testc/obj/x86_64-linux-gnu/Makefile.tmp /usr/bin/make /cvc3-2.4.1/testc/bin/x86_64-linux-gnu/testc make[4]: Entering directory '/cvc3-2.4.1/testc' gcc -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -g -I../src/include -o /cvc3-2.4.1/testc/obj/x86_64-linux-gnu/main.o -c main.c main.c: In function ‘test1’: main.c:79:8: warning: unused variable ‘k’ [-Wunused-variable] Kind k; ^ main.c: In function ‘test5’: main.c:399:17: warning: unused variable ‘p’ [-Wunused-variable] Expr x, xEQx, p; ^ main.c: In function ‘test6’: main.c:429:9: warning: unused variable ‘x’ [-Wunused-variable] char *x; ^ main.c:428:15: warning: unused variable ‘p32’ [-Wunused-variable] Expr p, p3, p32; ^ main.c:428:11: warning: unused variable ‘p3’ [-Wunused-variable] Expr p, p3, p32; ^ main.c:428:8: warning: unused variable ‘p’ [-Wunused-variable] Expr p, p3, p32; ^ g++ -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wall -I. -I/cvc3-2.4.1/src/include -Wl,-z,relro -o '/cvc3-2.4.1/testc/bin/x86_64-linux-gnu/testc' \ /cvc3-2.4.1/testc/obj/x86_64-linux-gnu/main.o -L/cvc3-2.4.1/lib/x86_64-linux-gnu -lcvc3 -lgmp make[4]: Leaving directory '/cvc3-2.4.1/testc' ln -sf /cvc3-2.4.1/testc/bin/x86_64-linux-gnu/testc /cvc3-2.4.1/testc/bin/testc make[3]: Leaving directory '/cvc3-2.4.1/testc' ********************************************************* Starting tests at Mon Aug 31 17:50:35 UTC 2015 C++ API test ********************************************************* /cvc3-2.4.1/test/bin/test 0 2>&1 \ | tee -a regressions.log; [ ${PIPESTATUS[0]} -eq 0 ] Running API test, regress level = 0 } test26(): { Query: ((x << 16)[31:0] = BVSHL(x,0bin00000000000000000000000000010000)) Valid Query: ((x >> 16) = BVLSHR(x,0bin00000000000000000000000000010000)) Valid Query: ((x >> 16) = BVASHR(x,0bin00000000000000000000000000010000)) Invalid test(): { Lambda application: (LAMBDA (x: INT): x)(1) Simplified: 1 } test1(): { Query: TRUE Valid Query: FALSE Invalid Query: (p OR NOT p) Valid Query: ((x = y) => (f(x) = f(y))) Valid Query: ((f(x) = f(y)) => (x = y)) Invalid Scope level: 4 Counter-example: NOT (y = x) (f(y) = f(x)) End of counter-example Resetting Scope level: 1 Push Scope Assert: (w = x) Assert: (x = y) Assert: (y = z) Assert: (f(x) = f(y)) Assert: (x = 1) simplify(w) = 1 Assert: (z = 2) Inconsistent?: 1 Assumptions Used: (z = 2) ((1 + (-1 * x)) = 0) (z = x) Pop Scope simplify(w) = w Inconsistent?: 0 } test2(): { Query: (b <= 10) Valid Query: FALSE Invalid Query: ((x = y) => (g(x, y) = g(y, x))) Valid Query: ((x = y) => (h(x, y) = h(y, x))) Valid } test3(): { i: 37 Trying test: ((((i - 1) < i) OR (((i - 1) = i) AND ((j - k) < j))) AND ((j < (j - k)) OR ((j = (j - k)) AND (i < (i - 1))))) Test Invalid Under Conditions: (0 <= k) Trying test under condition: NOT (0 <= k) Result Valid } test4(): { i: 37 Trying test: ((((i - 1) < i) OR (((i - 1) = i) AND ((j - k) < j))) AND ((j < (j - k)) OR ((j = (j - k)) AND (i < (i - 1))))) Test Invalid Under Conditions: (0 <= k) Trying test under condition: NOT (0 <= k) Result Valid } test6(): { vc1 variables: x, y vc2 variables: x, y vars imported to vc2 from vc1: x, y *** VC #1: Assert: (LET v_1 = f(5), v_0 = (# bar := v_1, foo := f(x) #) IN (v_0 = (v_0 WITH .foo := v_1))) Assert: ((ar WITH [x] := (# bar := f(5), foo := f(x) #)) = ar) Query: ((ar[x]).foo = ((# bar := f(5), foo := f(x) #)).bar) Valid *** VC #2: Assert: (LET v_1 = f(5), v_0 = (# bar := v_1, foo := f(x) #) IN (v_0 = (v_0 WITH .foo := v_1))) Assert: ((ar WITH [x] := (# bar := f(5), foo := f(x) #)) = ar) Query: ((ar[x]).foo = ((# bar := f(5), foo := f(x) #)).bar) Valid } test7(): { Assert: (e1 = e2) } test8(): { } test9(10): { Query: (LET v_0 = (a0 AND FALSE), v_1 = (b0 AND FALSE), v_2 = ((a0 AND b0) OR (v_1 OR v_0)), v_4 = ((a1 AND b1) OR ((b1 AND v_2) OR (a1 AND v_2))), v_6 = ((a2 AND b2) OR ((b2 AND v_4) OR (a2 AND v_4))), v_8 = ((a3 AND b3) OR ((b3 AND v_6) OR (a3 AND v_6))), v_10 = ((a4 AND b4) OR ((b4 AND v_8) OR (a4 AND v_8))), v_12 = ((a5 AND b5) OR ((b5 AND v_10) OR (a5 AND v_10))), v_14 = ((a6 AND b6) OR ((b6 AND v_12) OR (a6 AND v_12))), v_16 = ((a7 AND b7) OR ((b7 AND v_14) OR (a7 AND v_14))), v_3 = ((b0 AND a0) OR (v_0 OR v_1)), v_5 = ((b1 AND a1) OR ((a1 AND v_3) OR (b1 AND v_3))), v_7 = ((b2 AND a2) OR ((a2 AND v_5) OR (b2 AND v_5))), v_9 = ((b3 AND a3) OR ((a3 AND v_7) OR (b3 AND v_7))), v_11 = ((b4 AND a4) OR ((a4 AND v_9) OR (b4 AND v_9))), v_13 = ((b5 AND a5) OR ((a5 AND v_11) OR (b5 AND v_11))), v_15 = ((b6 AND a6) OR ((a6 AND v_13) OR (b6 AND v_13))), v_17 = ((b7 AND a7) OR ((a7 AND v_15) OR (b7 AND v_15))) IN ((((((((((TRUE AND (NOT (NOT (a0 <=> b0) <=> FALSE) <=> NOT (NOT (b0 <=> a0) <=> FALSE))) AND (NOT (NOT (a1 <=> b1) <=> v_2) <=> NOT (NOT (b1 <=> a1) <=> v_3))) AND (NOT (NOT (a2 <=> b2) <=> v_4) <=> NOT (NOT (b2 <=> a2) <=> v_5))) AND (NOT (NOT (a3 <=> b3) <=> v_6) <=> NOT (NOT (b3 <=> a3) <=> v_7))) AND (NOT (NOT (a4 <=> b4) <=> v_8) <=> NOT (NOT (b4 <=> a4) <=> v_9))) AND (NOT (NOT (a5 <=> b5) <=> v_10) <=> NOT (NOT (b5 <=> a5) <=> v_11))) AND (NOT (NOT (a6 <=> b6) <=> v_12) <=> NOT (NOT (b6 <=> a6) <=> v_13))) AND (NOT (NOT (a7 <=> b7) <=> v_14) <=> NOT (NOT (b7 <=> a7) <=> v_15))) AND (NOT (NOT (a8 <=> b8) <=> v_16) <=> NOT (NOT (b8 <=> a8) <=> v_17))) AND (NOT (NOT (a9 <=> b9) <=> ((a8 AND b8) OR ((b8 AND v_16) OR (a8 AND v_16)))) <=> NOT (NOT (b9 <=> a9) <=> ((b8 AND a8) OR ((a8 AND v_17) OR (b8 AND v_17))))))) Valid bvtest9(): { Query: (LET v_0 = BVPLUS(2, a, b), v_1 = (a)[0:0], v_2 = (b)[0:0] IN (((0bin1 & BVXNOR((v_0)[0:0],BVXOR(v_1,BVXOR(v_2,0bin0)))) & BVXNOR((v_0)[1:1],BVXOR((a)[1:1],BVXOR((b)[1:1],((v_1 & v_2) | ((v_2 & 0bin0) | (v_1 & 0bin0))))))) = 0bin1)) Valid } test10[0] test11(): { Push Assert x = y Implied Literals: (y = x) (x = y) (f(x) = f(y)) Push Assert x /= z Implied Literals: NOT (z = x) NOT (y = z) NOT (z = y) NOT (x = z) Pop Push Assert y /= z Implied Literals: NOT (z = x) NOT (y = z) NOT (z = y) NOT (x = z) Pop Push Assert p(x) Implied Literals: p(x) p(y) Pop Push Assert p(y) Implied Literals: p(x) p(y) Pop Pop Push Assert y = x Implied Literals: (y = x) (x = y) (f(x) = f(y)) Pop Push Assert p(x) Implied Literals: p(x) Assert x = y Implied Literals: (y = x) p(y) (x = y) (f(x) = f(y)) Pop Push Assert NOT p(x) Implied Literals: NOT p(x) Assert x = y Implied Literals: (y = x) NOT p(y) (x = y) (f(x) = f(y)) Pop } test12(): { } test13(): { 2=1 0 2=-1 0 } test14(): { } test15(): { Query: (FORALL (id: [0..2]) : (((((array WITH [0] := 1) WITH [1] := 1) WITH [2] := 0) WITH [3] := 0)[id] <= ((((array WITH [0] := 1) WITH [1] := 1) WITH [2] := 0) WITH [3] := 0)[(id + 1)])) Invalid Scope level: 5 Counter-example: NOT (FORALL (_BD1TY0: [0..2]) : (((((array WITH [0] := 1) WITH [1] := 1) WITH [2] := 0) WITH [3] := 0)[_BD1TY0] <= ((((array WITH [0] := 1) WITH [1] := 1) WITH [2] := 0) WITH [3] := 0)[(_BD1TY0 + 1)])) NOT (SKOLEM_268 <= SKOLEM_277) NOT ((2 + (-1 * SKOLEM_72)) = 0) (SKOLEM_268 = SKOLEM_391) (SKOLEM_457 = SKOLEM_483) ((1 + (-1 * SKOLEM_72)) = 0) (SKOLEM_277 = 0) (SKOLEM_391 = 1) NOT (SKOLEM_268 = 0) NOT ((1 + SKOLEM_72) = 0) (SKOLEM_483 = array[(1 + SKOLEM_72)]) NOT (SKOLEM_72 = 0) (SKOLEM_471 = array[SKOLEM_72]) NOT ((3 + (-1 * SKOLEM_72)) = 0) (SKOLEM_431 = SKOLEM_471) NOT ((-1 * SKOLEM_72) = 0) (SKOLEM_405 = SKOLEM_457) End of counter-example Checking forallExpr <==> manual expansion ... -- yes. Checking !forallExpr <==> existsExpr ... -- yes. End of testcases. } test16(): { Query: (NOT (a = b) => ((mem WITH [a] := 30)[b] = (mem WITH [b] := 40)[a])) Invalid Scope level: 4 Counter-example: NOT (b = a) NOT (mem[a] = mem[b]) (0 <= (-1 + (-1 * b) + a)) NOT (0 <= (-1 + b + (-1 * a))) End of counter-example %Satisfiable Variable Assignment: % ASSERT (mem = (ARRAY (arr_var: [0..100]): IF (arr_var = 1) THEN 0 ELSE 1 ENDIF)); ASSERT (a = 1); ASSERT (b = 0); ASSERT (mem[1] = 0); ASSERT (mem[0] = 1); } test17(): { Query: (car(cons(x, y)) = x) Valid Query: (((z = cons1(x, y)) AND is_null(y)) => (z = cons1(x, null))) Valid Query: NOT (NOT (x = y) AND NOT (y = z) AND NOT (x = z)) Valid } test18(): { Query: NOT (zero = null) Query: (succ(pred(x)) = x) Query: (is_succ(x) => (succ(pred(x)) = x)) Valid Query: (is_zero(x) OR is_succ(x)) Valid Query: ((x = y) => (succ(x) = succ(y))) Valid Query: NOT (succ(x) = zero) Valid Query: ((succ(x) = succ(y)) => (x = y)) Valid Query: NOT (succ(x) = x) Valid } test19(): { Checking formula (Hs[t6] = Ht[t6]) in context (FORALL (CVCi: REAL) : (Hs[CVCi] = Ht[CVCi])) test20(): { 0: p(a, cons(0bin00, (ARRAY (_cvc3_: INT): 0))) 1: p(a, cons(0bin01, (ARRAY (_cvc3_: INT): 0))) 2: p(a, cons(0bin10, (ARRAY (_cvc3_: INT): 0))) 3: p(a, cons(0bin11, (ARRAY (_cvc3_: INT): 0))) 4: p(b, cons(0bin00, (ARRAY (_cvc3_: INT): 0))) 5: p(b, cons(0bin01, (ARRAY (_cvc3_: INT): 0))) 6: p(b, cons(0bin10, (ARRAY (_cvc3_: INT): 0))) 7: p(b, cons(0bin11, (ARRAY (_cvc3_: INT): 0))) 8: p(c, cons(0bin00, (ARRAY (_cvc3_: INT): 0))) 9: p(c, cons(0bin01, (ARRAY (_cvc3_: INT): 0))) 10: p(c, cons(0bin10, (ARRAY (_cvc3_: INT): 0))) 11: p(c, cons(0bin11, (ARRAY (_cvc3_: INT): 0))) 12: p(d, cons(0bin00, (ARRAY (_cvc3_: INT): 0))) 13: p(d, cons(0bin01, (ARRAY (_cvc3_: INT): 0))) 14: p(d, cons(0bin10, (ARRAY (_cvc3_: INT): 0))) 15: p(d, cons(0bin11, (ARRAY (_cvc3_: INT): 0))) 16: p(e, cons(0bin00, (ARRAY (_cvc3_: INT): 0))) 17: p(e, cons(0bin01, (ARRAY (_cvc3_: INT): 0))) 18: p(e, cons(0bin10, (ARRAY (_cvc3_: INT): 0))) 19: p(e, cons(0bin11, (ARRAY (_cvc3_: INT): 0))) } test21(): { x1: x x2: x y1: y y2: y a1: (x > 0) a2: (x > 0) b1: (x < y) b2: (x < y) e1: ((x > 0) AND (x < y)) e2: ((x > 0) AND (x < y)) } test22(): { } test23(): { s=(x < y) t=(a < b) u=(a < b) } test24(): { (FORALL (x: INT) : PATTERN (a[x]) : (x < a[x])) (FORALL (x: INT) : PATTERN (a'[x]) : (x < a'[x])) } test25(): { -0.1: -1/10 -1/10: -1/10 -1 over 10: -1/10 -1 over 10 (ints): -1/10 } Program exits successfully. ********************************************************* C API test ********************************************************* /cvc3-2.4.1/testc/bin/testc 0 2>&1 \ | tee -a regressions.log; [ ${PIPESTATUS[0]} -eq 0 ] Running C API test, regress level = 0 test1() { Query: (p OR NOT p) Valid Query: ((x = y) => (f(x) = f(y))) Valid Query: ((f(x) = f(y)) => (x = y)) Invalid Stack level: 1 Counter-example: NOT (y = x) (f(y) = f(x)) End of counter-example Concrete model: (p = TRUE) (x = 1/4) (y = 0) (f = (LAMBDA (uf_0: REAL): 0)) (f(1/4) = 0) (f(0) = 0) End of concrete model Resetting Stack level: 0 Push Scope Assert: (w = x) Assert: (x = y) Assert: (y = z) Assert: (f(x) = f(y)) Assert: (x = 1) Assert: (x = 2) simplify(w) = 1 Inconsistent?: 1 Assumptions Used: (x = 2) ((1 + (-1 * x)) = 0) Pop Scope simplify(w) = w Inconsistent?: 0 } test2() { Query: ((x = y) => (g(x, y) = g(y, x))) Valid Query: ((x = y) => (h(x, y) = h(y, x))) Valid } test4() { } test5() { } test7() { Push Assert x = y Implied Literals: (y = x) (x = y) (f(x) = f(y)) Push Assert x /= z Implied Literals: NOT (z = x) NOT (y = z) NOT (z = y) NOT (x = z) Pop Pop } test10() { eq: 1 } test11() { } ********************************************************* Java API test ********************************************************* /usr/bin/make -C java test 2>&1 \ | tee -a regressions.log; [ ${PIPESTATUS[0]} -eq 0 ] make[3]: Entering directory '/cvc3-2.4.1/java' if [ ! -d /cvc3-2.4.1/java/lib ]; then mkdir -p /cvc3-2.4.1/java/lib; fi if [ ! -d obj ]; then mkdir -p obj; fi /usr/lib/jvm/default-java/bin/java -d64 -Djava.library.path=../java/lib/x86_64-linux-gnu -ea -jar ../java/lib/cvc3test.jar Running API test, regress level = 3 test(): Lambda application: (LAMBDA (x: INT): x)(1) Simplified: 1 } test1(): Query: TRUE Valid Query: FALSE Invalid Query: (p OR NOT p) Valid Query: ((x = y) => (f(x) = f(y))) Valid Query: ((f(x) = f(y)) => (x = y)) Invalid Scope level: 4 Counter-example: NOT (y = x) (f(y) = f(x)) End of counter-example Resetting Scope level: 1 Push Scope Assert: (w = x) Assert: (x = y) Assert: (y = z) Assert: (f(x) = f(y)) Assert: (x = 1) simplify(w) = 1 Assert: (z = 2) Inconsistent?: true Assumptions Used: (z = 2) ((1 + (-1 * x)) = 0) (z = x) Pop Scope simplify(w) = w Inconsistent?: false } test2(): Query: (b <= 10) Valid Query: FALSE Invalid Query: ((x = y) => (g(x, y) = g(y, x))) Valid Query: ((x = y) => (h(x, y) = h(y, x))) Valid } test3(): Trying test: ((((i - 1) < i) OR (((i - 1) = i) AND ((j - k) < j))) AND ((j < (j - k)) OR ((j = (j - k)) AND (i < (i - 1))))) Test Invalid Under Conditions: (0 <= k) Trying test under condition: NOT (0 <= k) Result Valid } test4(): Trying test: ((((i - 1) < i) OR (((i - 1) = i) AND ((j - k) < j))) AND ((j < (j - k)) OR ((j = (j - k)) AND (i < (i - 1))))) Test Invalid Under Conditions: (0 <= k) Trying test under condition: NOT (0 <= k) Result Valid } test5(): Checking verification condition:(((i1 < i2)) => (((M WITH [(q + i1)] := M[(r + i1)]) WITH [(p + i2)] := (M WITH [(q + i1)] := M[(r + i1)])[(r + i2)])[arb_addr] = ((M WITH [(p + i2)] := M[(r + i2)]) WITH [(q + i1)] := (M WITH [(p + i2)] := M[(r + i2)])[(r + i1)])[arb_addr])) Invalid Under Conditions: NOT (0 <= (0 + (-1 * i2) + i1)) NOT (SKOLEM_318 = SKOLEM_327) ((0 + arb_addr + (-1 * q) + (-1 * i1)) = 0) (SKOLEM_318 = SKOLEM_339) (SKOLEM_373 = M[(0 + r + i1)]) ((0 + r + (-1 * p) + (-1 * i2) + i1) = 0) (SKOLEM_339 = M[(0 + r + i2)]) NOT ((0 + arb_addr + (-1 * p) + (-1 * i2)) = 0) (SKOLEM_327 = SKOLEM_373) (SKOLEM_350 = M[arb_addr]) NOT (SKOLEM_339 = M[(0 + r + i1)]) (arb_addr = (0 + r + i2)) ((0 + (-1 * r) + q + (-1 * i2) + i1) = 0) (SKOLEM_362 = M[(0 + r + i1)]) (SKOLEM_350 = M[(0 + r + i2)]) (SKOLEM_318 = SKOLEM_350) NOT (SKOLEM_373 = M[arb_addr]) NOT (SKOLEM_362 = M[(0 + r + i2)]) (SKOLEM_327 = SKOLEM_362) Condition ineligible: negation: NOT (0 <= (0 + (-1 * i2) + i1)) Condition ineligible: negation: NOT (SKOLEM_318 = SKOLEM_327) Condition ineligible: not enough non-loop variables: ((0 + arb_addr + (-1 * q) + (-1 * i1)) = 0) Condition selected: (SKOLEM_318 = SKOLEM_339) Trying verification condition with hypothesis: (NOT (SKOLEM_318 = SKOLEM_339)) Invalid Under Conditions: NOT (0 <= (0 + (-1 * i2) + i1)) NOT (SKOLEM_318 = SKOLEM_327) ((0 + arb_addr + (-1 * q) + (-1 * i1)) = 0) (SKOLEM_318 = SKOLEM_339) (SKOLEM_373 = M[(0 + r + i1)]) ((0 + r + (-1 * p) + (-1 * i2) + i1) = 0) (SKOLEM_339 = M[(0 + r + i2)]) NOT ((0 + arb_addr + (-1 * p) + (-1 * i2)) = 0) (SKOLEM_327 = SKOLEM_373) (SKOLEM_350 = M[arb_addr]) NOT (SKOLEM_339 = M[(0 + r + i1)]) (arb_addr = (0 + r + i2)) ((0 + (-1 * r) + q + (-1 * i2) + i1) = 0) (SKOLEM_362 = M[(0 + r + i1)]) (SKOLEM_350 = M[(0 + r + i2)]) (SKOLEM_318 = SKOLEM_350) NOT (SKOLEM_373 = M[arb_addr]) NOT (SKOLEM_362 = M[(0 + r + i2)]) (SKOLEM_327 = SKOLEM_362) Attempting to remove loop variables Loop variables successfully removed: (NOT (SKOLEM_318 = SKOLEM_339)) Final query Result Invalid } test6(): vc1 variables: x, y vc2 variables: x, y vars imported to vc2 from vc1: x, y *** VC #1: Assert: (LET v_1 = f(5), v_0 = (# bar := v_1, foo := f(x) #) IN (v_0 = (v_0 WITH .foo := v_1))) Assert: ((ar WITH [x] := (# bar := f(5), foo := f(x) #)) = ar) Query: ((ar[x]).foo = ((# bar := f(5), foo := f(x) #)).bar) Valid *** VC #2: Assert: (LET v_1 = f(5), v_0 = (# bar := v_1, foo := f(x) #) IN (v_0 = (v_0 WITH .foo := v_1))) Assert: ((ar WITH [x] := (# bar := f(5), foo := f(x) #)) = ar) Query: ((ar[x]).foo = ((# bar := f(5), foo := f(x) #)).bar) Valid } test7(): Assert: (e1 = e2) } test8(): } test9(): Query: (LET v_1 = (b0 AND FALSE), v_0 = (a0 AND FALSE), v_2 = ((a0 AND b0) OR (v_1 OR v_0)), v_4 = ((a1 AND b1) OR ((b1 AND v_2) OR (a1 AND v_2))), v_6 = ((a2 AND b2) OR ((b2 AND v_4) OR (a2 AND v_4))), v_8 = ((a3 AND b3) OR ((b3 AND v_6) OR (a3 AND v_6))), v_10 = ((a4 AND b4) OR ((b4 AND v_8) OR (a4 AND v_8))), v_12 = ((a5 AND b5) OR ((b5 AND v_10) OR (a5 AND v_10))), v_14 = ((a6 AND b6) OR ((b6 AND v_12) OR (a6 AND v_12))), v_16 = ((a7 AND b7) OR ((b7 AND v_14) OR (a7 AND v_14))), v_18 = ((a8 AND b8) OR ((b8 AND v_16) OR (a8 AND v_16))), v_20 = ((a9 AND b9) OR ((b9 AND v_18) OR (a9 AND v_18))), v_22 = ((a10 AND b10) OR ((b10 AND v_20) OR (a10 AND v_20))), v_24 = ((a11 AND b11) OR ((b11 AND v_22) OR (a11 AND v_22))), v_26 = ((a12 AND b12) OR ((b12 AND v_24) OR (a12 AND v_24))), v_28 = ((a13 AND b13) OR ((b13 AND v_26) OR (a13 AND v_26))), v_30 = ((a14 AND b14) OR ((b14 AND v_28) OR (a14 AND v_28))), v_32 = ((a15 AND b15) OR ((b15 AND v_30) OR (a15 AND v_30))), v_34 = ((a16 AND b16) OR ((b16 AND v_32) OR (a16 AND v_32))), v_36 = ((a17 AND b17) OR ((b17 AND v_34) OR (a17 AND v_34))), v_38 = ((a18 AND b18) OR ((b18 AND v_36) OR (a18 AND v_36))), v_40 = ((a19 AND b19) OR ((b19 AND v_38) OR (a19 AND v_38))), v_42 = ((a20 AND b20) OR ((b20 AND v_40) OR (a20 AND v_40))), v_44 = ((a21 AND b21) OR ((b21 AND v_42) OR (a21 AND v_42))), v_46 = ((a22 AND b22) OR ((b22 AND v_44) OR (a22 AND v_44))), v_48 = ((a23 AND b23) OR ((b23 AND v_46) OR (a23 AND v_46))), v_50 = ((a24 AND b24) OR ((b24 AND v_48) OR (a24 AND v_48))), v_52 = ((a25 AND b25) OR ((b25 AND v_50) OR (a25 AND v_50))), v_54 = ((a26 AND b26) OR ((b26 AND v_52) OR (a26 AND v_52))), v_56 = ((a27 AND b27) OR ((b27 AND v_54) OR (a27 AND v_54))), v_58 = ((a28 AND b28) OR ((b28 AND v_56) OR (a28 AND v_56))), v_60 = ((a29 AND b29) OR ((b29 AND v_58) OR (a29 AND v_58))), v_62 = ((a30 AND b30) OR ((b30 AND v_60) OR (a30 AND v_60))), v_64 = ((a31 AND b31) OR ((b31 AND v_62) OR (a31 AND v_62))), v_66 = ((a32 AND b32) OR ((b32 AND v_64) OR (a32 AND v_64))), v_68 = ((a33 AND b33) OR ((b33 AND v_66) OR (a33 AND v_66))), v_70 = ((a34 AND b34) OR ((b34 AND v_68) OR (a34 AND v_68))), v_72 = ((a35 AND b35) OR ((b35 AND v_70) OR (a35 AND v_70))), v_74 = ((a36 AND b36) OR ((b36 AND v_72) OR (a36 AND v_72))), v_76 = ((a37 AND b37) OR ((b37 AND v_74) OR (a37 AND v_74))), v_3 = ((b0 AND a0) OR (v_0 OR v_1)), v_5 = ((b1 AND a1) OR ((a1 AND v_3) OR (b1 AND v_3))), v_7 = ((b2 AND a2) OR ((a2 AND v_5) OR (b2 AND v_5))), v_9 = ((b3 AND a3) OR ((a3 AND v_7) OR (b3 AND v_7))), v_11 = ((b4 AND a4) OR ((a4 AND v_9) OR (b4 AND v_9))), v_13 = ((b5 AND a5) OR ((a5 AND v_11) OR (b5 AND v_11))), v_15 = ((b6 AND a6) OR ((a6 AND v_13) OR (b6 AND v_13))), v_17 = ((b7 AND a7) OR ((a7 AND v_15) OR (b7 AND v_15))), v_19 = ((b8 AND a8) OR ((a8 AND v_17) OR (b8 AND v_17))), v_21 = ((b9 AND a9) OR ((a9 AND v_19) OR (b9 AND v_19))), v_23 = ((b10 AND a10) OR ((a10 AND v_21) OR (b10 AND v_21))), v_25 = ((b11 AND a11) OR ((a11 AND v_23) OR (b11 AND v_23))), v_27 = ((b12 AND a12) OR ((a12 AND v_25) OR (b12 AND v_25))), v_29 = ((b13 AND a13) OR ((a13 AND v_27) OR (b13 AND v_27))), v_31 = ((b14 AND a14) OR ((a14 AND v_29) OR (b14 AND v_29))), v_33 = ((b15 AND a15) OR ((a15 AND v_31) OR (b15 AND v_31))), v_35 = ((b16 AND a16) OR ((a16 AND v_33) OR (b16 AND v_33))), v_37 = ((b17 AND a17) OR ((a17 AND v_35) OR (b17 AND v_35))), v_39 = ((b18 AND a18) OR ((a18 AND v_37) OR (b18 AND v_37))), v_41 = ((b19 AND a19) OR ((a19 AND v_39) OR (b19 AND v_39))), v_43 = ((b20 AND a20) OR ((a20 AND v_41) OR (b20 AND v_41))), v_45 = ((b21 AND a21) OR ((a21 AND v_43) OR (b21 AND v_43))), v_47 = ((b22 AND a22) OR ((a22 AND v_45) OR (b22 AND v_45))), v_49 = ((b23 AND a23) OR ((a23 AND v_47) OR (b23 AND v_47))), v_51 = ((b24 AND a24) OR ((a24 AND v_49) OR (b24 AND v_49))), v_53 = ((b25 AND a25) OR ((a25 AND v_51) OR (b25 AND v_51))), v_55 = ((b26 AND a26) OR ((a26 AND v_53) OR (b26 AND v_53))), v_57 = ((b27 AND a27) OR ((a27 AND v_55) OR (b27 AND v_55))), v_59 = ((b28 AND a28) OR ((a28 AND v_57) OR (b28 AND v_57))), v_61 = ((b29 AND a29) OR ((a29 AND v_59) OR (b29 AND v_59))), v_63 = ((b30 AND a30) OR ((a30 AND v_61) OR (b30 AND v_61))), v_65 = ((b31 AND a31) OR ((a31 AND v_63) OR (b31 AND v_63))), v_67 = ((b32 AND a32) OR ((a32 AND v_65) OR (b32 AND v_65))), v_69 = ((b33 AND a33) OR ((a33 AND v_67) OR (b33 AND v_67))), v_71 = ((b34 AND a34) OR ((a34 AND v_69) OR (b34 AND v_69))), v_73 = ((b35 AND a35) OR ((a35 AND v_71) OR (b35 AND v_71))), v_75 = ((b36 AND a36) OR ((a36 AND v_73) OR (b36 AND v_73))), v_77 = ((b37 AND a37) OR ((a37 AND v_75) OR (b37 AND v_75))) IN ((((((((((((((((((((((((((((((((((((((((TRUE AND (NOT (NOT (a0 <=> b0) <=> FALSE) <=> NOT (NOT (b0 <=> a0) <=> FALSE))) AND (NOT (NOT (a1 <=> b1) <=> v_2) <=> NOT (NOT (b1 <=> a1) <=> v_3))) AND (NOT (NOT (a2 <=> b2) <=> v_4) <=> NOT (NOT (b2 <=> a2) <=> v_5))) AND (NOT (NOT (a3 <=> b3) <=> v_6) <=> NOT (NOT (b3 <=> a3) <=> v_7))) AND (NOT (NOT (a4 <=> b4) <=> v_8) <=> NOT (NOT (b4 <=> a4) <=> v_9))) AND (NOT (NOT (a5 <=> b5) <=> v_10) <=> NOT (NOT (b5 <=> a5) <=> v_11))) AND (NOT (NOT (a6 <=> b6) <=> v_12) <=> NOT (NOT (b6 <=> a6) <=> v_13))) AND (NOT (NOT (a7 <=> b7) <=> v_14) <=> NOT (NOT (b7 <=> a7) <=> v_15))) AND (NOT (NOT (a8 <=> b8) <=> v_16) <=> NOT (NOT (b8 <=> a8) <=> v_17))) AND (NOT (NOT (a9 <=> b9) <=> v_18) <=> NOT (NOT (b9 <=> a9) <=> v_19))) AND (NOT (NOT (a10 <=> b10) <=> v_20) <=> NOT (NOT (b10 <=> a10) <=> v_21))) AND (NOT (NOT (a11 <=> b11) <=> v_22) <=> NOT (NOT (b11 <=> a11) <=> v_23))) AND (NOT (NOT (a12 <=> b12) <=> v_24) <=> NOT (NOT (b12 <=> a12) <=> v_25))) AND (NOT (NOT (a13 <=> b13) <=> v_26) <=> NOT (NOT (b13 <=> a13) <=> v_27))) AND (NOT (NOT (a14 <=> b14) <=> v_28) <=> NOT (NOT (b14 <=> a14) <=> v_29))) AND (NOT (NOT (a15 <=> b15) <=> v_30) <=> NOT (NOT (b15 <=> a15) <=> v_31))) AND (NOT (NOT (a16 <=> b16) <=> v_32) <=> NOT (NOT (b16 <=> a16) <=> v_33))) AND (NOT (NOT (a17 <=> b17) <=> v_34) <=> NOT (NOT (b17 <=> a17) <=> v_35))) AND (NOT (NOT (a18 <=> b18) <=> v_36) <=> NOT (NOT (b18 <=> a18) <=> v_37))) AND (NOT (NOT (a19 <=> b19) <=> v_38) <=> NOT (NOT (b19 <=> a19) <=> v_39))) AND (NOT (NOT (a20 <=> b20) <=> v_40) <=> NOT (NOT (b20 <=> a20) <=> v_41))) AND (NOT (NOT (a21 <=> b21) <=> v_42) <=> NOT (NOT (b21 <=> a21) <=> v_43))) AND (NOT (NOT (a22 <=> b22) <=> v_44) <=> NOT (NOT (b22 <=> a22) <=> v_45))) AND (NOT (NOT (a23 <=> b23) <=> v_46) <=> NOT (NOT (b23 <=> a23) <=> v_47))) AND (NOT (NOT (a24 <=> b24) <=> v_48) <=> NOT (NOT (b24 <=> a24) <=> v_49))) AND (NOT (NOT (a25 <=> b25) <=> v_50) <=> NOT (NOT (b25 <=> a25) <=> v_51))) AND (NOT (NOT (a26 <=> b26) <=> v_52) <=> NOT (NOT (b26 <=> a26) <=> v_53))) AND (NOT (NOT (a27 <=> b27) <=> v_54) <=> NOT (NOT (b27 <=> a27) <=> v_55))) AND (NOT (NOT (a28 <=> b28) <=> v_56) <=> NOT (NOT (b28 <=> a28) <=> v_57))) AND (NOT (NOT (a29 <=> b29) <=> v_58) <=> NOT (NOT (b29 <=> a29) <=> v_59))) AND (NOT (NOT (a30 <=> b30) <=> v_60) <=> NOT (NOT (b30 <=> a30) <=> v_61))) AND (NOT (NOT (a31 <=> b31) <=> v_62) <=> NOT (NOT (b31 <=> a31) <=> v_63))) AND (NOT (NOT (a32 <=> b32) <=> v_64) <=> NOT (NOT (b32 <=> a32) <=> v_65))) AND (NOT (NOT (a33 <=> b33) <=> v_66) <=> NOT (NOT (b33 <=> a33) <=> v_67))) AND (NOT (NOT (a34 <=> b34) <=> v_68) <=> NOT (NOT (b34 <=> a34) <=> v_69))) AND (NOT (NOT (a35 <=> b35) <=> v_70) <=> NOT (NOT (b35 <=> a35) <=> v_71))) AND (NOT (NOT (a36 <=> b36) <=> v_72) <=> NOT (NOT (b36 <=> a36) <=> v_73))) AND (NOT (NOT (a37 <=> b37) <=> v_74) <=> NOT (NOT (b37 <=> a37) <=> v_75))) AND (NOT (NOT (a38 <=> b38) <=> v_76) <=> NOT (NOT (b38 <=> a38) <=> v_77))) AND (NOT (NOT (a39 <=> b39) <=> ((a38 AND b38) OR ((b38 AND v_76) OR (a38 AND v_76)))) <=> NOT (NOT (b39 <=> a39) <=> ((b38 AND a38) OR ((a38 AND v_77) OR (b38 AND v_77))))))) Valid } bvtest9(): Query: (LET v_0 = BVPLUS(11, a, b), v_1 = (a)[0:0], v_2 = (b)[0:0], v_3 = (a)[1:1], v_4 = (b)[1:1], v_6 = (a)[2:2], v_7 = (b)[2:2], v_9 = (a)[3:3], v_10 = (b)[3:3], v_12 = (a)[4:4], v_13 = (b)[4:4], v_15 = (a)[5:5], v_16 = (b)[5:5], v_18 = (a)[6:6], v_19 = (b)[6:6], v_21 = (a)[7:7], v_22 = (b)[7:7], v_24 = (a)[8:8], v_25 = (b)[8:8], v_27 = (a)[9:9], v_28 = (b)[9:9], v_5 = ((v_1 & v_2) | ((v_2 & 0bin0) | (v_1 & 0bin0))), v_8 = ((v_3 & v_4) | ((v_4 & v_5) | (v_3 & v_5))), v_11 = ((v_6 & v_7) | ((v_7 & v_8) | (v_6 & v_8))), v_14 = ((v_9 & v_10) | ((v_10 & v_11) | (v_9 & v_11))), v_17 = ((v_12 & v_13) | ((v_13 & v_14) | (v_12 & v_14))), v_20 = ((v_15 & v_16) | ((v_16 & v_17) | (v_15 & v_17))), v_23 = ((v_18 & v_19) | ((v_19 & v_20) | (v_18 & v_20))), v_26 = ((v_21 & v_22) | ((v_22 & v_23) | (v_21 & v_23))), v_29 = ((v_24 & v_25) | ((v_25 & v_26) | (v_24 & v_26))) IN ((((((((((((0bin1 & BVXNOR((v_0)[0:0],BVXOR(v_1,BVXOR(v_2,0bin0)))) & BVXNOR((v_0)[1:1],BVXOR(v_3,BVXOR(v_4,v_5)))) & BVXNOR((v_0)[2:2],BVXOR(v_6,BVXOR(v_7,v_8)))) & BVXNOR((v_0)[3:3],BVXOR(v_9,BVXOR(v_10,v_11)))) & BVXNOR((v_0)[4:4],BVXOR(v_12,BVXOR(v_13,v_14)))) & BVXNOR((v_0)[5:5],BVXOR(v_15,BVXOR(v_16,v_17)))) & BVXNOR((v_0)[6:6],BVXOR(v_18,BVXOR(v_19,v_20)))) & BVXNOR((v_0)[7:7],BVXOR(v_21,BVXOR(v_22,v_23)))) & BVXNOR((v_0)[8:8],BVXOR(v_24,BVXOR(v_25,v_26)))) & BVXNOR((v_0)[9:9],BVXOR(v_27,BVXOR(v_28,v_29)))) & BVXNOR((v_0)[10:10],BVXOR((a)[10:10],BVXOR((b)[10:10],((v_27 & v_28) | ((v_28 & v_29) | (v_27 & v_29))))))) = 0bin1)) Valid test10[0] test10[100] test10[200] test10[300] } test11(): Push Assert x = y Implied Literals: (y = x) (x = y) (f(x) = f(y)) Push Assert x /= z Implied Literals: NOT (z = x) NOT (y = z) NOT (z = y) NOT (x = z) Pop Push Assert y /= z Implied Literals: NOT (z = x) NOT (y = z) NOT (z = y) NOT (x = z) Pop Push Assert p(x) Implied Literals: p(x) p(y) Pop Push Assert p(y) Implied Literals: p(x) p(y) Pop Pop Push Assert y = x Implied Literals: (y = x) (x = y) (f(x) = f(y)) Pop Push Assert p(x) Implied Literals: p(x) Assert x = y Implied Literals: (y = x) p(y) (x = y) (f(x) = f(y)) Pop Push Assert NOT p(x) Implied Literals: NOT p(x) Assert x = y Implied Literals: (y = x) NOT p(y) (x = y) (f(x) = f(y)) Pop } test12(): } test13(): 2=1 INVALID 2=-1 INVALID } test14(): } test15(): Query: (FORALL (id: [0..2]) : (((((array WITH [0] := 1) WITH [1] := 1) WITH [2] := 0) WITH [3] := 0)[id] <= ((((array WITH [0] := 1) WITH [1] := 1) WITH [2] := 0) WITH [3] := 0)[(id + 1)])) Invalid Scope level: 5 Counter-example: NOT (FORALL (_BD1TY0: [0..2]) : (((((array WITH [0] := 1) WITH [1] := 1) WITH [2] := 0) WITH [3] := 0)[_BD1TY0] <= ((((array WITH [0] := 1) WITH [1] := 1) WITH [2] := 0) WITH [3] := 0)[(_BD1TY0 + 1)])) NOT (SKOLEM_268 <= SKOLEM_277) NOT ((2 + (-1 * SKOLEM_72)) = 0) (SKOLEM_268 = SKOLEM_391) (SKOLEM_457 = SKOLEM_483) ((1 + (-1 * SKOLEM_72)) = 0) (SKOLEM_277 = 0) (SKOLEM_391 = 1) NOT (SKOLEM_268 = 0) NOT ((1 + SKOLEM_72) = 0) (SKOLEM_483 = array[(1 + SKOLEM_72)]) NOT (SKOLEM_72 = 0) (SKOLEM_471 = array[SKOLEM_72]) NOT ((3 + (-1 * SKOLEM_72)) = 0) (SKOLEM_431 = SKOLEM_471) NOT ((-1 * SKOLEM_72) = 0) (SKOLEM_405 = SKOLEM_457) End of counter-example Checking forallExpr <==> manual expansion ... -- yes. Checking !forallExpr <==> existsExpr ... -- yes. End of testcases. } test16(): Query: (NOT (a = b) => ((mem WITH [a] := 30)[b] = (mem WITH [b] := 40)[a])) Invalid Scope level: 4 Counter-example: NOT (b = a) NOT (mem[a] = mem[b]) (0 <= (-1 + (-1 * b) + a)) NOT (0 <= (-1 + b + (-1 * a))) End of counter-example %Satisfiable Variable Assignment: % (a = 1) (mem[1] = 0) (mem[0] = 1) (b = 0) (mem = (ARRAY (arr_var: [0..100]): IF (arr_var = 1) THEN 0 ELSE 1 ENDIF)) } test17(): Query: (car(cons(x, y)) = x) Valid Query: NOT (NOT (x = y) AND NOT (y = z) AND NOT (x = z)) Valid } test18(): Query: NOT (zero = null) Query: (succ(pred(x)) = x) Query: (is_succ(x) => (succ(pred(x)) = x)) Valid Query: (is_zero(x) OR is_succ(x)) Valid Query: ((x = y) => (succ(x) = succ(y))) Valid Query: NOT (succ(x) = zero) Valid Query: ((succ(x) = succ(y)) => (x = y)) Valid Query: NOT (succ(x) = x) Valid } test19(): Checking formula (Hs[t6] = Ht[t6]) in context (FORALL (CVCi: REAL) : (Hs[CVCi] = Ht[CVCi])) } test22(): } test23(): s=(x < y) t=(a < b) u=(a < b) } testNonlinearBV(): Checking BVUDIV: Query: (NOT (0bin00000000 = y) => BVLE(BVMULT(8,BVUDIV(x,y),y),x)) Valid Checking BVUREM: Query: (NOT (0bin00000000 = y) => BVLT(BVUREM(x,y),y)) Valid Checking BVSDIV: Query: ((BVSLE(0bin00000000,x) AND BVSLT(0bin00000000,y)) => BVSLE(BVMULT(8,BVSDIV(x,y),y),x)) Valid Checking BVSREM: Query: ((BVSLE(0bin00000000,x) AND BVSLT(0bin00000000,y)) => BVLT(BVSREM(x,y),y)) Valid Checking BVSMOD: Query: ((BVSLE(0bin00000000,x) AND BVSLT(0bin00000000,y)) => BVLT(BVSMOD(x,y),y)) Valid } testDistinct(): Query: NOT DISTINCT(x0, x1, x2, x3, x4) Valid } Program exits successfully. make[3]: Leaving directory '/cvc3-2.4.1/java' ********************************************************* Regression tests ********************************************************* /cvc3-2.4.1/bin/run_tests -l 0 -vc /cvc3-2.4.1/bin/cvc3 +rt -t 1200 benchmarks -- +stats 2>&1 \ | tee -a regressions.log; [ ${PIPESTATUS[0]} -eq 0 ] ********* Regression level: 0 Language: all Whether to produce / check proofs: depends on testcase Time limit per test: 1200 sec PATH = /cvc3-2.4.1/bin/:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin ********* *** WARNING: cannot find testcase benchmarks: no such file or directory Statistics: Total tests run: 0 Total running time: 0 sec Total elapsed time: 0 sec Total number of proofs checked: 0 Problematic cases: 0 ********************************************************* Output is saved in regressions.log ********************************************************* make[2]: Leaving directory '/cvc3-2.4.1' make[1]: Leaving directory '/cvc3-2.4.1' touch debian/stamp-makefile-check debian/rules binary test -x debian/rules dh_testroot dh_prep dh_installdirs -A mkdir -p "." if test -e /usr/share/misc/config.guess ; then \ for i in ./config.guess ; do \ if ! test -e $i.cdbs-orig ; then \ mv $i $i.cdbs-orig ; \ cp --remove-destination /usr/share/misc/config.guess $i ; \ fi ; \ done ; \ fi if test -e /usr/share/misc/config.sub ; then \ for i in ./config.sub ; do \ if ! test -e $i.cdbs-orig ; then \ mv $i $i.cdbs-orig ; \ cp --remove-destination /usr/share/misc/config.sub $i ; \ fi ; \ done ; \ fi /usr/bin/make -C . install prefix=/cvc3-2.4.1/debian/tmp//usr make[1]: Entering directory '/cvc3-2.4.1' /usr/bin/make TARGET=install make[2]: Entering directory '/cvc3-2.4.1' cd /cvc3-2.4.1/src; /usr/bin/make install VERSION=2.4.1 make[3]: Entering directory '/cvc3-2.4.1/src' /usr/bin/make build TARGET= make[4]: Entering directory '/cvc3-2.4.1/src' cd util && /usr/bin/make make[5]: Entering directory '/cvc3-2.4.1/src/util' make[5]: Nothing to be done for 'all'. make[5]: Leaving directory '/cvc3-2.4.1/src/util' cd context && /usr/bin/make make[5]: Entering directory '/cvc3-2.4.1/src/context' make[5]: Nothing to be done for 'all'. make[5]: Leaving directory '/cvc3-2.4.1/src/context' cd expr && /usr/bin/make make[5]: Entering directory '/cvc3-2.4.1/src/expr' make[5]: Nothing to be done for 'all'. make[5]: Leaving directory '/cvc3-2.4.1/src/expr' cd theorem && /usr/bin/make make[5]: Entering directory '/cvc3-2.4.1/src/theorem' make[5]: Nothing to be done for 'all'. make[5]: Leaving directory '/cvc3-2.4.1/src/theorem' cd sat && /usr/bin/make make[5]: Entering directory '/cvc3-2.4.1/src/sat' make[5]: Nothing to be done for 'all'. make[5]: Leaving directory '/cvc3-2.4.1/src/sat' cd theory_core && /usr/bin/make make[5]: Entering directory '/cvc3-2.4.1/src/theory_core' make[5]: Nothing to be done for 'all'. make[5]: Leaving directory '/cvc3-2.4.1/src/theory_core' cd theory_arith && /usr/bin/make make[5]: Entering directory '/cvc3-2.4.1/src/theory_arith' make[5]: Nothing to be done for 'all'. make[5]: Leaving directory '/cvc3-2.4.1/src/theory_arith' cd theory_array && /usr/bin/make make[5]: Entering directory '/cvc3-2.4.1/src/theory_array' make[5]: Nothing to be done for 'all'. make[5]: Leaving directory '/cvc3-2.4.1/src/theory_array' cd theory_bitvector && /usr/bin/make make[5]: Entering directory '/cvc3-2.4.1/src/theory_bitvector' make[5]: Nothing to be done for 'all'. make[5]: Leaving directory '/cvc3-2.4.1/src/theory_bitvector' cd theory_datatype && /usr/bin/make make[5]: Entering directory '/cvc3-2.4.1/src/theory_datatype' make[5]: Nothing to be done for 'all'. make[5]: Leaving directory '/cvc3-2.4.1/src/theory_datatype' cd theory_quant && /usr/bin/make make[5]: Entering directory '/cvc3-2.4.1/src/theory_quant' make[5]: Nothing to be done for 'all'. make[5]: Leaving directory '/cvc3-2.4.1/src/theory_quant' cd theory_records && /usr/bin/make make[5]: Entering directory '/cvc3-2.4.1/src/theory_records' make[5]: Nothing to be done for 'all'. make[5]: Leaving directory '/cvc3-2.4.1/src/theory_records' cd theory_simulate && /usr/bin/make make[5]: Entering directory '/cvc3-2.4.1/src/theory_simulate' make[5]: Nothing to be done for 'all'. make[5]: Leaving directory '/cvc3-2.4.1/src/theory_simulate' cd theory_uf && /usr/bin/make make[5]: Entering directory '/cvc3-2.4.1/src/theory_uf' make[5]: Nothing to be done for 'all'. make[5]: Leaving directory '/cvc3-2.4.1/src/theory_uf' cd search && /usr/bin/make make[5]: Entering directory '/cvc3-2.4.1/src/search' make[5]: Nothing to be done for 'all'. make[5]: Leaving directory '/cvc3-2.4.1/src/search' cd parser && /usr/bin/make make[5]: Entering directory '/cvc3-2.4.1/src/parser' make[5]: Nothing to be done for 'all'. make[5]: Leaving directory '/cvc3-2.4.1/src/parser' cd translator && /usr/bin/make make[5]: Entering directory '/cvc3-2.4.1/src/translator' make[5]: Nothing to be done for 'all'. make[5]: Leaving directory '/cvc3-2.4.1/src/translator' cd vcl && /usr/bin/make make[5]: Entering directory '/cvc3-2.4.1/src/vcl' make[5]: Nothing to be done for 'all'. make[5]: Leaving directory '/cvc3-2.4.1/src/vcl' cd c_interface && /usr/bin/make make[5]: Entering directory '/cvc3-2.4.1/src/c_interface' make[5]: Nothing to be done for 'all'. make[5]: Leaving directory '/cvc3-2.4.1/src/c_interface' /usr/bin/make /cvc3-2.4.1/lib/libcvc3.so.5.0.0 make[5]: Entering directory '/cvc3-2.4.1/src' ln -sf /cvc3-2.4.1/lib/x86_64-linux-gnu/libcvc3.so.5.0.0 '/cvc3-2.4.1/lib//libcvc3.so.5.0.0' /sbin/ldconfig -nv '/cvc3-2.4.1/lib/' /cvc3-2.4.1/lib: libcvc3.so.5 -> libcvc3.so.5.0.0 ln -sf libcvc3.so.5.0.0 '/cvc3-2.4.1/lib//libcvc3.so.5.0' ln -sf libcvc3.so.5.0.0 '/cvc3-2.4.1/lib//libcvc3.so.5' ln -sf libcvc3.so.5.0.0 '/cvc3-2.4.1/lib//libcvc3.so' make[5]: Leaving directory '/cvc3-2.4.1/src' cd cvc3 && /usr/bin/make VERSION=2.4.1 make[5]: Entering directory '/cvc3-2.4.1/src/cvc3' /usr/bin/make /cvc3-2.4.1/bin/x86_64-linux-gnu/cvc3 make[6]: Entering directory '/cvc3-2.4.1/src/cvc3' make[6]: '/cvc3-2.4.1/bin/x86_64-linux-gnu/cvc3' is up to date. make[6]: Leaving directory '/cvc3-2.4.1/src/cvc3' ln -sf /cvc3-2.4.1/bin/x86_64-linux-gnu/cvc3 /cvc3-2.4.1/bin/cvc3 make[5]: Leaving directory '/cvc3-2.4.1/src/cvc3' make[4]: Leaving directory '/cvc3-2.4.1/src' mkdir -p /cvc3-2.4.1/debian/tmp//usr/include/cvc3 /usr/bin/install -m 644 /cvc3-2.4.1/src/include/assumptions.h /cvc3-2.4.1/src/include/c_interface.h /cvc3-2.4.1/src/include/c_interface_defs.h /cvc3-2.4.1/src/include/cdflags.h /cvc3-2.4.1/src/include/cdlist.h /cvc3-2.4.1/src/include/cdmap.h /cvc3-2.4.1/src/include/cdmap_ordered.h /cvc3-2.4.1/src/include/cdo.h /cvc3-2.4.1/src/include/circuit.h /cvc3-2.4.1/src/include/clause.h /cvc3-2.4.1/src/include/cnf.h /cvc3-2.4.1/src/include/cnf_manager.h /cvc3-2.4.1/src/include/command_line_exception.h /cvc3-2.4.1/src/include/command_line_flags.h /cvc3-2.4.1/src/include/common_proof_rules.h /cvc3-2.4.1/src/include/compat_hash_map.h /cvc3-2.4.1/src/include/compat_hash_set.h /cvc3-2.4.1/src/include/context.h /cvc3-2.4.1/src/include/cvc_util.h /cvc3-2.4.1/src/include/debug.h /cvc3-2.4.1/src/include/dpllt.h /cvc3-2.4.1/src/include/dpllt_basic.h /cvc3-2.4.1/src/include/dpllt_minisat.h /cvc3-2.4.1/src/include/eval_exception.h /cvc3-2.4.1/src/include/exception.h /cvc3-2.4.1/src/include/expr.h /cvc3-2.4.1/src/include/expr_hash.h /cvc3-2.4.1/src/include/expr_manager.h /cvc3-2.4.1/src/include/expr_map.h /cvc3-2.4.1/src/include/expr_op.h /cvc3-2.4.1/src/include/expr_stream.h /cvc3-2.4.1/src/include/expr_transform.h /cvc3-2.4.1/src/include/expr_value.h /cvc3-2.4.1/src/include/formula_value.h /cvc3-2.4.1/src/include/fdstream.h /cvc3-2.4.1/src/include/hash_fun.h /cvc3-2.4.1/src/include/hash_table.h /cvc3-2.4.1/src/include/hash_map.h /cvc3-2.4.1/src/include/hash_set.h /cvc3-2.4.1/src/include/kinds.h /cvc3-2.4.1/src/include/lang.h /cvc3-2.4.1/src/include/memory_manager.h /cvc3-2.4.1/src/include/memory_manager_chunks.h /cvc3-2.4.1/src/include/memory_manager_malloc.h /cvc3-2.4.1/src/include/memory_manager_context.h /cvc3-2.4.1/src/include/notifylist.h /cvc3-2.4.1/src/include/os.h /cvc3-2.4.1/src/include/parser.h /cvc3-2.4.1/src/include/proof.h /cvc3-2.4.1/src/include/rational.h /cvc3-2.4.1/src/include/parser_exception.h /cvc3-2.4.1/src/include/pretty_printer.h /cvc3-2.4.1/src/include/queryresult.h /cvc3-2.4.1/src/include/sat_api.h /cvc3-2.4.1/src/include/search.h /cvc3-2.4.1/src/include/search_impl_base.h /cvc3-2.4.1/src/include/search_sat.h /cvc3-2.4.1/src/include/search_simple.h /cvc3-2.4.1/src/include/search_fast.h /cvc3-2.4.1/src/include/smartcdo.h /cvc3-2.4.1/src/include/smtlib_exception.h /cvc3-2.4.1/src/include/sound_exception.h /cvc3-2.4.1/src/include/statistics.h /cvc3-2.4.1/src/include/theorem.h /cvc3-2.4.1/src/include/theorem_manager.h /cvc3-2.4.1/src/include/theorem_producer.h /cvc3-2.4.1/src/include/theory_arith.h /cvc3-2.4.1/src/include/theory_arith_new.h /cvc3-2.4.1/src/include/theory_arith_old.h /cvc3-2.4.1/src/include/theory_arith3.h /cvc3-2.4.1/src/include/theory_array.h /cvc3-2.4.1/src/include/theory_bitvector.h /cvc3-2.4.1/src/include/theory_core.h /cvc3-2.4.1/src/include/theory_datatype.h /cvc3-2.4.1/src/include/theory_datatype_lazy.h /cvc3-2.4.1/src/include/theory.h /cvc3-2.4.1/src/include/theory_quant.h /cvc3-2.4.1/src/include/theory_records.h /cvc3-2.4.1/src/include/theory_simulate.h /cvc3-2.4.1/src/include/theory_uf.h /cvc3-2.4.1/src/include/translator.h /cvc3-2.4.1/src/include/typecheck_exception.h /cvc3-2.4.1/src/include/type.h /cvc3-2.4.1/src/include/variable.h /cvc3-2.4.1/src/include/vc_cmd.h /cvc3-2.4.1/src/include/vc.h /cvc3-2.4.1/src/include/vcl.h /cvc3-2.4.1/debian/tmp//usr/include/cvc3 mkdir -p /cvc3-2.4.1/debian/tmp//usr/lib /usr/bin/install -m 644 /cvc3-2.4.1/lib/libcvc3.so.5.0.0 /cvc3-2.4.1/debian/tmp//usr/lib /sbin/ldconfig -nv /cvc3-2.4.1/debian/tmp//usr/lib /cvc3-2.4.1/debian/tmp//usr/lib: libcvc3.so.5 -> libcvc3.so.5.0.0 (changed) ln -sf libcvc3.so.5.0.0 /cvc3-2.4.1/debian/tmp//usr/lib/libcvc3.so.5.0 ln -sf libcvc3.so.5.0.0 /cvc3-2.4.1/debian/tmp//usr/lib/libcvc3.so.5 ln -sf libcvc3.so.5.0.0 /cvc3-2.4.1/debian/tmp//usr/lib/libcvc3.so mkdir -p /cvc3-2.4.1/debian/tmp//usr/bin /usr/bin/install -m 755 /cvc3-2.4.1/bin/cvc3 /cvc3-2.4.1/debian/tmp//usr/bin mkdir -p /cvc3-2.4.1/debian/tmp//usr/lib/pkgconfig /usr/bin/install -m 644 cvc3.pc /cvc3-2.4.1/debian/tmp//usr/lib/pkgconfig make[3]: Leaving directory '/cvc3-2.4.1/src' cd /cvc3-2.4.1/java; /usr/bin/make install VERSION=2.4.1 make[3]: Entering directory '/cvc3-2.4.1/java' if [ ! -d obj ]; then mkdir -p obj; fi if [ ! -d /cvc3-2.4.1/java/lib/x86_64-linux-gnu ]; then mkdir -p /cvc3-2.4.1/java/lib/x86_64-linux-gnu; fi g++ -shared -g -O2 -fstack-protector-strong -Wformat -Werror=format-security -Wall -m64 -fPIC -O2 -Wl,-z,relro \ -Wl,-soname,libcvc3jni.so.5.0 \ -L ../lib obj/cvc3/*.o \ -o /cvc3-2.4.1/java/lib/x86_64-linux-gnu/libcvc3jni.so.5.0.0 -lcvc3 -lgmp /sbin/ldconfig -nv /cvc3-2.4.1/java/lib/x86_64-linux-gnu /cvc3-2.4.1/java/lib/x86_64-linux-gnu: libcvc3jni.so.5.0 -> libcvc3jni.so.5.0.0 ln -sf libcvc3jni.so.5.0.0 /cvc3-2.4.1/java/lib/x86_64-linux-gnu/libcvc3jni.so.5.0 ln -sf libcvc3jni.so.5.0.0 /cvc3-2.4.1/java/lib/x86_64-linux-gnu/libcvc3jni.so.5 ln -sf libcvc3jni.so.5.0.0 /cvc3-2.4.1/java/lib/x86_64-linux-gnu/libcvc3jni.so mkdir -p /cvc3-2.4.1/debian/tmp//usr/java /usr/bin/install -m 644 /cvc3-2.4.1/java/lib/libcvc3-5.0.0.jar /cvc3-2.4.1/debian/tmp//usr/java mkdir -p /cvc3-2.4.1/debian/tmp//usr/lib /usr/bin/install -m 644 /cvc3-2.4.1/java/lib/x86_64-linux-gnu/libcvc3jni.so.5.0.0 /cvc3-2.4.1/debian/tmp//usr/lib ln -sf libcvc3jni.so.5.0.0 /cvc3-2.4.1/debian/tmp//usr/lib/libcvc3jni.so.5 ln -sf libcvc3jni.so.5.0.0 /cvc3-2.4.1/debian/tmp//usr/lib/libcvc3jni.so.5.0 ln -sf libcvc3jni.so.5.0.0 /cvc3-2.4.1/debian/tmp//usr/lib/libcvc3jni.so /sbin/ldconfig -nv /cvc3-2.4.1/debian/tmp//usr/lib /cvc3-2.4.1/debian/tmp//usr/lib: libcvc3jni.so.5.0 -> libcvc3jni.so.5.0.0 libcvc3.so.5 -> libcvc3.so.5.0.0 make[3]: Leaving directory '/cvc3-2.4.1/java' make[2]: Leaving directory '/cvc3-2.4.1' make[1]: Leaving directory '/cvc3-2.4.1' touch debian/stamp-makefile-install Adding cdbs dependencies to debian/libcvc3-5-java.substvars dh_installdirs -plibcvc3-5-java Adding cdbs dependencies to debian/cvc3-el.substvars dh_installdirs -pcvc3-el install -m 755 -d debian/cvc3-el/usr/share/emacs/site-lisp/cvc3-el install -m 644 emacs/cvc-mode.el debian/cvc3-el/usr/share/emacs/site-lisp/cvc3-el dh_installdocs -plibcvc3-5-java ./README dh_installexamples -plibcvc3-5-java dh_installman -plibcvc3-5-java dh_installinfo -plibcvc3-5-java dh_installmenu -plibcvc3-5-java dh_installcron -plibcvc3-5-java dh_installinit -plibcvc3-5-java dh_installdebconf -plibcvc3-5-java dh_installemacsen -plibcvc3-5-java dh_installcatalogs -plibcvc3-5-java dh_installpam -plibcvc3-5-java dh_installlogrotate -plibcvc3-5-java dh_installlogcheck -plibcvc3-5-java dh_installchangelogs -plibcvc3-5-java dh_installudev -plibcvc3-5-java dh_lintian -plibcvc3-5-java dh_bugfiles -plibcvc3-5-java dh_install -plibcvc3-5-java dh_systemd_enable -plibcvc3-5-java dh_systemd_start -plibcvc3-5-java dh_link -plibcvc3-5-java dh_installmime -plibcvc3-5-java dh_installgsettings -plibcvc3-5-java dh_installdocs -pcvc3-el ./README dh_installexamples -pcvc3-el dh_installman -pcvc3-el dh_installinfo -pcvc3-el dh_installmenu -pcvc3-el dh_installcron -pcvc3-el dh_installinit -pcvc3-el dh_installdebconf -pcvc3-el dh_installemacsen -pcvc3-el dh_installcatalogs -pcvc3-el dh_installpam -pcvc3-el dh_installlogrotate -pcvc3-el dh_installlogcheck -pcvc3-el dh_installchangelogs -pcvc3-el dh_installudev -pcvc3-el dh_lintian -pcvc3-el dh_bugfiles -pcvc3-el dh_install -pcvc3-el dh_systemd_enable -pcvc3-el dh_systemd_start -pcvc3-el dh_link -pcvc3-el dh_installmime -pcvc3-el dh_installgsettings -pcvc3-el dh_strip -plibcvc3-5-java dh_compress -plibcvc3-5-java dh_fixperms -plibcvc3-5-java dh_makeshlibs -plibcvc3-5-java dh_strip -pcvc3-el dh_compress -pcvc3-el dh_fixperms -pcvc3-el dh_makeshlibs -pcvc3-el dh_installdeb -plibcvc3-5-java dh_perl -plibcvc3-5-java dh_shlibdeps -plibcvc3-5-java dh_installdeb -pcvc3-el dh_perl -pcvc3-el dh_shlibdeps -pcvc3-el dh_gencontrol -plibcvc3-5-java dpkg-gencontrol: warning: Depends field of package libcvc3-5-java: unknown substitution variable ${shlibs:Depends} dh_md5sums -plibcvc3-5-java dh_builddeb -plibcvc3-5-java dpkg-deb: building package 'libcvc3-5-java' in '../libcvc3-5-java_2.4.1-5_all.deb'. dh_gencontrol -pcvc3-el dh_md5sums -pcvc3-el dh_builddeb -pcvc3-el dpkg-deb: building package 'cvc3-el' in '../cvc3-el_2.4.1-5_all.deb'. Adding cdbs dependencies to debian/cvc3.substvars dh_installdirs -pcvc3 Adding cdbs dependencies to debian/libcvc3-5.substvars dh_installdirs -plibcvc3-5 Adding cdbs dependencies to debian/libcvc3-dev.substvars dh_installdirs -plibcvc3-dev Adding cdbs dependencies to debian/libcvc3-5-jni.substvars dh_installdirs -plibcvc3-5-jni dh_installdocs -pcvc3 ./README dh_installexamples -pcvc3 dh_installman -pcvc3 dh_installinfo -pcvc3 dh_installmenu -pcvc3 dh_installcron -pcvc3 dh_installinit -pcvc3 dh_installdebconf -pcvc3 dh_installemacsen -pcvc3 dh_installcatalogs -pcvc3 dh_installpam -pcvc3 dh_installlogrotate -pcvc3 dh_installlogcheck -pcvc3 dh_installchangelogs -pcvc3 dh_installudev -pcvc3 dh_lintian -pcvc3 dh_bugfiles -pcvc3 dh_install -pcvc3 dh_systemd_enable -pcvc3 dh_systemd_start -pcvc3 dh_link -pcvc3 dh_installmime -pcvc3 dh_installgsettings -pcvc3 dh_installdocs -plibcvc3-5 ./README dh_installexamples -plibcvc3-5 dh_installman -plibcvc3-5 dh_installinfo -plibcvc3-5 dh_installmenu -plibcvc3-5 dh_installcron -plibcvc3-5 dh_installinit -plibcvc3-5 dh_installdebconf -plibcvc3-5 dh_installemacsen -plibcvc3-5 dh_installcatalogs -plibcvc3-5 dh_installpam -plibcvc3-5 dh_installlogrotate -plibcvc3-5 dh_installlogcheck -plibcvc3-5 dh_installchangelogs -plibcvc3-5 dh_installudev -plibcvc3-5 dh_lintian -plibcvc3-5 dh_bugfiles -plibcvc3-5 dh_install -plibcvc3-5 dh_systemd_enable -plibcvc3-5 dh_systemd_start -plibcvc3-5 dh_link -plibcvc3-5 dh_installmime -plibcvc3-5 dh_installgsettings -plibcvc3-5 dh_installdocs -plibcvc3-dev ./README dh_installexamples -plibcvc3-dev dh_installman -plibcvc3-dev dh_installinfo -plibcvc3-dev dh_installmenu -plibcvc3-dev dh_installcron -plibcvc3-dev dh_installinit -plibcvc3-dev dh_installdebconf -plibcvc3-dev dh_installemacsen -plibcvc3-dev dh_installcatalogs -plibcvc3-dev dh_installpam -plibcvc3-dev dh_installlogrotate -plibcvc3-dev dh_installlogcheck -plibcvc3-dev dh_installchangelogs -plibcvc3-dev dh_installudev -plibcvc3-dev dh_lintian -plibcvc3-dev dh_bugfiles -plibcvc3-dev dh_install -plibcvc3-dev dh_systemd_enable -plibcvc3-dev dh_systemd_start -plibcvc3-dev dh_link -plibcvc3-dev dh_installmime -plibcvc3-dev dh_installgsettings -plibcvc3-dev dh_installdocs -plibcvc3-5-jni ./README dh_installexamples -plibcvc3-5-jni dh_installman -plibcvc3-5-jni dh_installinfo -plibcvc3-5-jni dh_installmenu -plibcvc3-5-jni dh_installcron -plibcvc3-5-jni dh_installinit -plibcvc3-5-jni dh_installdebconf -plibcvc3-5-jni dh_installemacsen -plibcvc3-5-jni dh_installcatalogs -plibcvc3-5-jni dh_installpam -plibcvc3-5-jni dh_installlogrotate -plibcvc3-5-jni dh_installlogcheck -plibcvc3-5-jni dh_installchangelogs -plibcvc3-5-jni dh_installudev -plibcvc3-5-jni dh_lintian -plibcvc3-5-jni dh_bugfiles -plibcvc3-5-jni dh_install -plibcvc3-5-jni dh_systemd_enable -plibcvc3-5-jni dh_systemd_start -plibcvc3-5-jni dh_link -plibcvc3-5-jni dh_installmime -plibcvc3-5-jni dh_installgsettings -plibcvc3-5-jni dh_strip -pcvc3 dh_compress -pcvc3 dh_fixperms -pcvc3 dh_makeshlibs -pcvc3 dh_strip -plibcvc3-5 dh_compress -plibcvc3-5 dh_fixperms -plibcvc3-5 dh_makeshlibs -plibcvc3-5 dh_strip -plibcvc3-dev dh_compress -plibcvc3-dev dh_fixperms -plibcvc3-dev dh_makeshlibs -plibcvc3-dev dh_strip -plibcvc3-5-jni dh_compress -plibcvc3-5-jni dh_fixperms -plibcvc3-5-jni dh_makeshlibs -plibcvc3-5-jni dh_installdeb -pcvc3 dh_perl -pcvc3 dh_shlibdeps -pcvc3 dpkg-shlibdeps: warning: package could avoid a useless dependency if debian/cvc3/usr/bin/cvc3 was not linked against libgmp.so.10 (it uses none of the library's symbols) dh_installdeb -plibcvc3-5 dh_perl -plibcvc3-5 dh_shlibdeps -plibcvc3-5 dh_installdeb -plibcvc3-dev dh_perl -plibcvc3-dev dh_shlibdeps -plibcvc3-dev dh_installdeb -plibcvc3-5-jni dh_perl -plibcvc3-5-jni dh_shlibdeps -plibcvc3-5-jni dpkg-shlibdeps: warning: package could avoid a useless dependency if debian/libcvc3-5-jni/usr/lib/jni/libcvc3jni.so.5.0.0 was not linked against libgmp.so.10 (it uses none of the library's symbols) dh_gencontrol -pcvc3 dh_md5sums -pcvc3 dh_builddeb -pcvc3 dpkg-deb: building package 'cvc3' in '../cvc3_2.4.1-5_amd64.deb'. dh_gencontrol -plibcvc3-5 dh_md5sums -plibcvc3-5 dh_builddeb -plibcvc3-5 dpkg-deb: building package 'libcvc3-5' in '../libcvc3-5_2.4.1-5_amd64.deb'. dh_gencontrol -plibcvc3-dev dpkg-gencontrol: warning: Depends field of package libcvc3-dev: unknown substitution variable ${shlibs:Depends} dh_md5sums -plibcvc3-dev dh_builddeb -plibcvc3-dev dpkg-deb: building package 'libcvc3-dev' in '../libcvc3-dev_2.4.1-5_amd64.deb'. dh_gencontrol -plibcvc3-5-jni dh_md5sums -plibcvc3-5-jni dh_builddeb -plibcvc3-5-jni dpkg-deb: building package 'libcvc3-5-jni' in '../libcvc3-5-jni_2.4.1-5_amd64.deb'. dpkg-genchanges >../cvc3_2.4.1-5_amd64.changes dpkg-genchanges: not including original source code in upload dpkg-source --after-build cvc3-2.4.1 dpkg-buildpackage: binary and diff upload (original source NOT included)