diff options
| -rwxr-xr-x | README.smtcomp2010 | 15 | ||||
| -rw-r--r-- | compilation-log | 1646 |
2 files changed, 1655 insertions, 6 deletions
diff --git a/README.smtcomp2010 b/README.smtcomp2010 index 9af6ad729..970df3ad5 100755 --- a/README.smtcomp2010 +++ b/README.smtcomp2010 @@ -3,15 +3,18 @@ # This is the version submitted to SMT-COMP 2010. # # It was checked out, clean, then compiled with this -# script on goedel.cims.nyu.edu. +# script on goedel.cims.nyu.edu. stdout/stderr were +# redirected to compilation-log, subsequently checked +# in. # ./autogen.sh ./configure competition make strip builds/bin/cvc4 -make check +# non-LRA tests may fail because thy reg is off +make -k check || true mkdir cvc4-1.0a0-smtcomp2010 -cp smtcomp2010-runscript cvc4-smtcomp2010/run -chmod 755 cvc4-smtcomp2010/run -cp builds/bin/cvc4 cvc4-smtcomp2010/cvc4 -tar cfzv cvc4-1.0a0-smtcomp2010 +cp smtcomp2010-runscript cvc4-1.0a0-smtcomp2010/run +chmod 755 cvc4-1.0a0-smtcomp2010/run +cp builds/bin/cvc4 cvc4-1.0a0-smtcomp2010/cvc4 +tar cfzv cvc4-1.0a0-smtcomp2010.tgz cvc4-1.0a0-smtcomp2010 diff --git a/compilation-log b/compilation-log new file mode 100644 index 000000000..4e236ebf7 --- /dev/null +++ b/compilation-log @@ -0,0 +1,1646 @@ ++ ./autogen.sh +Preparing the cvc4 build system...please wait + +Found GNU Autoconf version 2.64 +Found GNU Automake version 1.11 +Found GNU Libtool version 2.2.6 + +Automatically preparing build ... done + +The cvc4 build system is now prepared. To build here, run: + ./configure + make ++ ./configure competition +: CVC4: building profile competition +checking build system type... x86_64-unknown-linux-gnu +checking host system type... x86_64-unknown-linux-gnu +checking target system type... x86_64-unknown-linux-gnu +checking for requested build profile... competition +checking for a BSD-compatible install... /usr/bin/install -c +checking whether build environment is sane... yes +checking for a thread-safe mkdir -p... /bin/mkdir -p +checking for gawk... gawk +checking whether make sets $(MAKE)... yes +checking for style of include used by make... GNU +checking for gcc... gcc +checking for C compiler default output file name... a.out +checking whether the C compiler works... yes +checking whether we are cross compiling... no +checking for suffix of executables... +checking for suffix of object files... o +checking whether we are using the GNU C compiler... yes +checking whether gcc accepts -g... yes +checking for gcc option to accept ISO C89... none needed +checking dependency style of gcc... gcc3 +checking for a sed that does not truncate output... /bin/sed +checking for grep that handles long lines and -e... /bin/grep +checking for egrep... /bin/grep -E +checking for fgrep... /bin/grep -F +checking for ld used by gcc... /usr/bin/ld +checking if the linker (/usr/bin/ld) is GNU ld... yes +checking for BSD- or MS-compatible name lister (nm)... /usr/bin/nm -B +checking the name lister (/usr/bin/nm -B) interface... BSD nm +checking whether ln -s works... yes +checking the maximum length of command line arguments... 1572864 +checking whether the shell understands some XSI constructs... yes +checking whether the shell understands "+="... yes +checking for /usr/bin/ld option to reload object files... -r +checking for objdump... objdump +checking how to recognize dependent libraries... pass_all +checking for ar... ar +checking for strip... strip +checking for ranlib... ranlib +checking command to parse /usr/bin/nm -B output from gcc object... ok +checking how to run the C preprocessor... gcc -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 for dlfcn.h... yes +checking for objdir... .libs +checking if gcc supports -fno-rtti -fno-exceptions... no +checking for gcc option to produce PIC... -fPIC -DPIC +checking if gcc PIC flag -fPIC -DPIC works... yes +checking if gcc static flag -static works... yes +checking if gcc supports -c -o file.o... yes +checking if gcc supports -c -o file.o... (cached) yes +checking whether the gcc linker (/usr/bin/ld -m elf_x86_64) supports shared libraries... yes +checking whether -lc should be explicitly linked in... no +checking dynamic linker characteristics... GNU/Linux ld.so +checking how to hardcode library paths into programs... immediate +checking whether stripping libraries is possible... yes +checking if libtool supports shared libraries... yes +checking whether to build shared libraries... yes +checking whether to build static libraries... no +checking for gcc... (cached) gcc +checking whether we are using the GNU C compiler... (cached) yes +checking whether gcc accepts -g... (cached) yes +checking for gcc option to accept ISO C89... (cached) none needed +checking dependency style of gcc... (cached) gcc3 +checking for g++... g++ +checking whether we are using the GNU C++ compiler... yes +checking whether g++ accepts -g... yes +checking dependency style of g++... gcc3 +checking whether we are using the GNU C++ compiler... (cached) yes +checking whether g++ accepts -g... (cached) yes +checking dependency style of g++... (cached) gcc3 +checking how to run the C++ preprocessor... g++ -E +checking for ld used by g++... /usr/bin/ld -m elf_x86_64 +checking if the linker (/usr/bin/ld -m elf_x86_64) is GNU ld... yes +checking whether the g++ linker (/usr/bin/ld -m elf_x86_64) supports shared libraries... yes +checking for g++ option to produce PIC... -fPIC -DPIC +checking if g++ PIC flag -fPIC -DPIC works... yes +checking if g++ static flag -static works... yes +checking if g++ supports -c -o file.o... yes +checking if g++ supports -c -o file.o... (cached) yes +checking whether the g++ linker (/usr/bin/ld -m elf_x86_64) supports shared libraries... yes +checking dynamic linker characteristics... GNU/Linux ld.so +checking how to hardcode library paths into programs... immediate +checking for pkg-config... /usr/bin/pkg-config +checking pkg-config is at least version 0.9.0... yes +checking for CLN... yes +checking for appropriate build string... competition +checking what dir to configure... builds/x86_64-unknown-linux-gnu/competition + +./config/mkbuilddir x86_64-unknown-linux-gnu competition +Setting up builds/x86_64-unknown-linux-gnu/competition... +removed `config.log' +removed `confdefs.h' +mkdir: created directory `builds' +mkdir: created directory `builds/x86_64-unknown-linux-gnu' +mkdir: created directory `builds/x86_64-unknown-linux-gnu/competition' +`builds/Makefile' -> `x86_64-unknown-linux-gnu/competition/Makefile.builds' +Creating builds/current... +Linking builds/src... +`builds/src' -> `x86_64-unknown-linux-gnu/competition/src' +Linking builds/test... +`builds/test' -> `x86_64-unknown-linux-gnu/competition/test' +cd builds/x86_64-unknown-linux-gnu/competition +../../../configure --with-build=competition +checking build system type... x86_64-unknown-linux-gnu +checking host system type... x86_64-unknown-linux-gnu +checking target system type... x86_64-unknown-linux-gnu +checking for requested build profile... competition +checking for a BSD-compatible install... /usr/bin/install -c +checking whether build environment is sane... yes +checking for a thread-safe mkdir -p... /bin/mkdir -p +checking for gawk... gawk +checking whether make sets $(MAKE)... yes +checking for style of include used by make... GNU +checking for gcc... gcc +checking for C compiler default output file name... a.out +checking whether the C compiler works... yes +checking whether we are cross compiling... no +checking for suffix of executables... +checking for suffix of object files... o +checking whether we are using the GNU C compiler... yes +checking whether gcc accepts -g... yes +checking for gcc option to accept ISO C89... none needed +checking dependency style of gcc... gcc3 +checking for a sed that does not truncate output... /bin/sed +checking for grep that handles long lines and -e... /bin/grep +checking for egrep... /bin/grep -E +checking for fgrep... /bin/grep -F +checking for ld used by gcc... /usr/bin/ld +checking if the linker (/usr/bin/ld) is GNU ld... yes +checking for BSD- or MS-compatible name lister (nm)... /usr/bin/nm -B +checking the name lister (/usr/bin/nm -B) interface... BSD nm +checking whether ln -s works... yes +checking the maximum length of command line arguments... 1572864 +checking whether the shell understands some XSI constructs... yes +checking whether the shell understands "+="... yes +checking for /usr/bin/ld option to reload object files... -r +checking for objdump... objdump +checking how to recognize dependent libraries... pass_all +checking for ar... ar +checking for strip... strip +checking for ranlib... ranlib +checking command to parse /usr/bin/nm -B output from gcc object... ok +checking how to run the C preprocessor... gcc -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 for dlfcn.h... yes +checking for objdir... .libs +checking if gcc supports -fno-rtti -fno-exceptions... no +checking for gcc option to produce PIC... -fPIC -DPIC +checking if gcc PIC flag -fPIC -DPIC works... yes +checking if gcc static flag -static works... yes +checking if gcc supports -c -o file.o... yes +checking if gcc supports -c -o file.o... (cached) yes +checking whether the gcc linker (/usr/bin/ld -m elf_x86_64) supports shared libraries... yes +checking whether -lc should be explicitly linked in... no +checking dynamic linker characteristics... GNU/Linux ld.so +checking how to hardcode library paths into programs... immediate +checking whether stripping libraries is possible... yes +checking if libtool supports shared libraries... yes +checking whether to build shared libraries... yes +checking whether to build static libraries... no +checking for gcc... (cached) gcc +checking whether we are using the GNU C compiler... (cached) yes +checking whether gcc accepts -g... (cached) yes +checking for gcc option to accept ISO C89... (cached) none needed +checking dependency style of gcc... (cached) gcc3 +checking for g++... g++ +checking whether we are using the GNU C++ compiler... yes +checking whether g++ accepts -g... yes +checking dependency style of g++... gcc3 +checking whether we are using the GNU C++ compiler... (cached) yes +checking whether g++ accepts -g... (cached) yes +checking dependency style of g++... (cached) gcc3 +checking how to run the C++ preprocessor... g++ -E +checking for ld used by g++... /usr/bin/ld -m elf_x86_64 +checking if the linker (/usr/bin/ld -m elf_x86_64) is GNU ld... yes +checking whether the g++ linker (/usr/bin/ld -m elf_x86_64) supports shared libraries... yes +checking for g++ option to produce PIC... -fPIC -DPIC +checking if g++ PIC flag -fPIC -DPIC works... yes +checking if g++ static flag -static works... yes +checking if g++ supports -c -o file.o... yes +checking if g++ supports -c -o file.o... (cached) yes +checking whether the g++ linker (/usr/bin/ld -m elf_x86_64) supports shared libraries... yes +checking dynamic linker characteristics... GNU/Linux ld.so +checking how to hardcode library paths into programs... immediate +checking for pkg-config... /usr/bin/pkg-config +checking pkg-config is at least version 0.9.0... yes +checking for CLN... yes +checking for appropriate build string... competition +checking what dir to configure... this one (in builds/) +checking whether to build a static binary... yes +checking whether to optimize libcvc4... yes +checking whether to include debugging symbols in libcvc4... no +checking whether to include statistics are turned on in libcvc4... no +checking whether to include assertions in build... no +checking whether to do a traceable build of CVC4... no +checking whether to do a muzzled build of CVC4... yes +checking whether to do a gcov-enabled build of CVC4... no +checking whether to do a profiling-enabled build of CVC4... no +checking for antlr3... /home/mdeters/bin/antlr3 +checking for doxygen... /usr/bin/doxygen +checking for perl... /usr/bin/perl +checking for cxxtestgen.pl... /home/mdeters/cxxtest/cxxtestgen.pl +checking for perl... perl +checking for ANTLR3 C runtime library... found in /home/mdeters/libantlr3 +checking getopt.h usability... yes +checking getopt.h presence... yes +checking for getopt.h... yes +checking for unistd.h... (cached) yes +: creating ./config.status +config.status: creating Makefile.builds +config.status: creating Makefile +config.status: creating contrib/Makefile +config.status: creating src/Makefile +config.status: creating src/context/Makefile +config.status: creating src/expr/Makefile +config.status: creating src/main/Makefile +config.status: creating src/parser/Makefile +config.status: creating src/parser/cvc/Makefile +config.status: creating src/parser/smt/Makefile +config.status: creating src/parser/smt2/Makefile +config.status: creating src/prop/Makefile +config.status: creating src/prop/minisat/Makefile +config.status: creating src/smt/Makefile +config.status: creating src/theory/Makefile +config.status: creating src/theory/arith/Makefile +config.status: creating src/theory/arrays/Makefile +config.status: creating src/theory/booleans/Makefile +config.status: creating src/theory/builtin/Makefile +config.status: creating src/theory/bv/Makefile +config.status: creating src/theory/uf/Makefile +config.status: creating src/util/Makefile +config.status: creating test/Makefile +config.status: creating test/regress/Makefile +config.status: creating test/regress/regress0/Makefile +config.status: creating test/regress/regress0/precedence/Makefile +config.status: creating test/regress/regress0/uf/Makefile +config.status: creating test/regress/regress1/Makefile +config.status: creating test/regress/regress2/Makefile +config.status: creating test/regress/regress3/Makefile +config.status: creating test/system/Makefile +config.status: creating test/unit/Makefile +config.status: creating src/util/rational.h +config.status: creating src/util/integer.h +config.status: creating cvc4autoconfig.h +config.status: executing depfiles commands +config.status: executing libtool commands + +CVC4 1.0a0-smtcomp2010 + +Build profile: competition +Build ID : competition +Optimized : yes, at level 9 +Debug symbols: no +Statistics : no +Assertions : no +Tracing : no +Muzzle : yes +gcov support : no +gprof support: no +Unit tests : unit testing infrastructure enabled in build directory + +Static libs : yes +Shared libs : no +Static binary: yes + +MP library : cln (GPL) + +CPPFLAGS : -DCVC4_COMPETITION_MODE -DCVC4_MUZZLE +CXXFLAGS : -funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs -O9 -Wno-deprecated +CFLAGS : -funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs -O9 -Wno-deprecated -fexceptions +LDFLAGS : + +libcvc4 version : 0:0:0 +libcvc4parser version: 0:0:0 + +Please note that CVC4 will be built against the Class Library for +Numbers (CLN). This library is covered under the GPL, so use of this +build of CVC4 will be more restrictive than CVC4's license would +normally suggest. For full details of CLN and its license, please visit + http://www.ginac.de/CLN/ +To build CVC4 with GMP instead (which is covered under the more permissive +LGPL), configure --without-cln. + +Now just type make, followed by make check or make install, as you like. + ++ make +cd builds +make all +make[1]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds' +(cd x86_64-unknown-linux-gnu/competition && make all) +make[2]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition' +make all-recursive +make[3]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition' +Making all in src +make[4]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src' +Making all in expr +make[5]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/expr' + GEN ../../src/theory/.subdirs + GEN kind.h + GEN metakind.h + GEN expr.h + GEN expr.cpp + GEN expr_manager.h + GEN expr_manager.cpp +make all-am +make[6]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/expr' + CXX node.lo + CXX type_node.lo + CXX type.lo + CXX attribute.lo + CXX node_manager.lo + CXX node_value.lo + CXX command.lo + CXX declaration_scope.lo + CXX expr.lo + CXX expr_manager.lo + CXXLD libexpr.la +make[6]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/expr' +make[5]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/expr' +Making all in util +make[5]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/util' +make all-am +make[6]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/util' + CXX Assert.lo + CXX decision_engine.lo + CXX output.lo + CXX configuration.lo + CXX bitvector.lo + CXX stats.lo + CXX integer_cln_imp.lo + CXX rational_cln_imp.lo + CXXLD libutil.la +make[6]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/util' +make[5]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/util' +Making all in context +make[5]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/context' + CXX context.lo + CXX context_mm.lo + CXXLD libcontext.la +make[5]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/context' +Making all in theory +make[5]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/theory' + GEN theoryof_table.h +make all-recursive +make[6]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/theory' +Making all in builtin +make[7]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/theory/builtin' + CXX theory_builtin.lo + CXXLD libbuiltin.la +make[7]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/theory/builtin' +Making all in booleans +make[7]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/theory/booleans' + CCLD libbooleans.la +make[7]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/theory/booleans' +Making all in uf +make[7]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/theory/uf' + CXX ecdata.lo + CXX theory_uf.lo + CXXLD libuf.la +make[7]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/theory/uf' +Making all in arith +make[7]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/theory/arith' + CXX arith_rewriter.lo +./../../expr/metakind.h: In function ‘bool pnfsMatch(CVC4::TNode, CVC4::TNode)’: +./../../expr/metakind.h:228: warning: array subscript is below array bounds +./../../expr/metakind.h:228: warning: array subscript is below array bounds +./../../expr/metakind.h:228: warning: array subscript is below array bounds +./../../expr/metakind.h:228: warning: array subscript is below array bounds +./../../expr/metakind.h: In member function ‘CVC4::Node CVC4::theory::arith::ArithRewriter::rewriteAtomCore(CVC4::TNode)’: +./../../expr/metakind.h:228: warning: array subscript is below array bounds + CXX delta_rational.lo + CXX partial_model.lo + CXX arith_propagator.lo + CXX theory_arith.lo +./../../expr/metakind.h: In function ‘bool isBasicSum(CVC4::TNode)’: +./../../expr/metakind.h:228: warning: array subscript is below array bounds +./../../expr/metakind.h:228: warning: array subscript is below array bounds +./../../expr/metakind.h: In function ‘bool isNormalAtom(CVC4::TNode)’: +./../../expr/metakind.h:228: warning: array subscript is below array bounds +./../../expr/metakind.h: In member function ‘CVC4::Node CVC4::theory::arith::TheoryArith::simulatePreprocessing(CVC4::TNode)’: +./../../expr/metakind.h:228: warning: array subscript is below array bounds +./../../expr/metakind.h: In member function ‘bool CVC4::theory::arith::TheoryArith::AssertEquality(CVC4::TNode, CVC4::TNode)’: +./../../expr/metakind.h:228: warning: array subscript is below array bounds +./../../expr/metakind.h: In member function ‘void CVC4::theory::arith::TheoryArith::setupSlack(CVC4::TNode)’: +./../../expr/metakind.h:228: warning: array subscript is below array bounds +./../../expr/metakind.h:228: warning: array subscript is below array bounds +./../../expr/metakind.h: In member function ‘virtual void CVC4::theory::arith::TheoryArith::preRegisterTerm(CVC4::TNode)’: +./../../expr/metakind.h:228: warning: array subscript is below array bounds + CXXLD libarith.la +make[7]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/theory/arith' +Making all in arrays +make[7]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/theory/arrays' + CXX theory_arrays.lo + CXXLD libarrays.la +make[7]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/theory/arrays' +Making all in bv +make[7]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/theory/bv' + CCLD libbv.la +make[7]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/theory/bv' +make[7]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/theory' + CXX theory_engine.lo + CXX theory.lo + CXX shared_term_manager.lo +./../expr/metakind.h: In member function ‘void CVC4::SharedTermManager::addEq(CVC4::TNode, CVC4::theory::Theory*)’: +./../expr/metakind.h:228: warning: array subscript is below array bounds +./../expr/metakind.h: In member function ‘CVC4::Node CVC4::SharedTermManager::explain(CVC4::TNode) const’: +./../expr/metakind.h:228: warning: array subscript is below array bounds + CXX shared_data.lo + CXXLD libtheory.la +make[7]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/theory' +make[6]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/theory' +make[5]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/theory' +Making all in prop +make[5]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/prop' +Making all in minisat +make[6]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/prop/minisat' + CXX Solver.lo + CXX SimpSolver.lo + CXXLD libminisat.la +make[6]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/prop/minisat' +make[6]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/prop' + CXX prop_engine.lo + CXX sat.lo + CXX cnf_stream.lo + CXXLD libprop.la +make[6]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/prop' +make[5]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/prop' +Making all in smt +make[5]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/smt' + CXX smt_engine.lo + CXXLD libsmt.la +make[5]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/smt' +Making all in . +make[5]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src' +touch empty.cpp + CXX empty.lo + CXXLD libcvc4_noinst.la + GEN libcvc4.la +make[5]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src' +Making all in parser +make[5]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/parser' +Making all in smt +make[6]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/parser/smt' + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../src/parser/smt/generated/SmtLexer.h +make all-am +make[7]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/parser/smt' + CXX smt.lo + CXX smt_input.lo + CC SmtLexer.lo + CC SmtParser.lo + CXXLD libparsersmt.la +make[7]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/parser/smt' +make[6]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/parser/smt' +Making all in smt2 +make[6]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/parser/smt2' + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../src/parser/smt2/generated/Smt2Lexer.h +make all-am +make[7]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/parser/smt2' + CXX smt2.lo + CXX smt2_input.lo + CC Smt2Lexer.lo + CC Smt2Parser.lo + CXXLD libparsersmt2.la +make[7]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/parser/smt2' +make[6]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/parser/smt2' +Making all in cvc +make[6]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/parser/cvc' + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../src/parser/cvc/generated/CvcLexer.h +make all-am +make[7]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/parser/cvc' + CXX cvc_input.lo + CC CvcLexer.lo + CC CvcParser.lo + CXXLD libparsercvc.la +make[7]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/parser/cvc' +make[6]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/parser/cvc' +make[6]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/parser' + CXX antlr_input.lo + CXX antlr_input_imports.lo + CXX bounded_token_buffer.lo + CXX bounded_token_factory.lo + CXX input.lo + CXX memory_mapped_input_buffer.lo + CXX parser.lo + CXX parser_builder.lo + CXXLD libcvc4parser_noinst.la + GEN libcvc4parser.la +make[6]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/parser' +make[5]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/parser' +Making all in main +make[5]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/main' + CXX main.o + CXX getopt.o + CXX util.o + GEN cvc4 +make[5]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/main' +make[4]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src' +Making all in test +make[4]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test' +Making all in unit +make[5]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit' +Makefile:977: .deps/theory/shared_term_manager_black.Plo: No such file or directory +Makefile:977: .deps/theory/theory_engine_white.Plo: No such file or directory +Makefile:977: .deps/theory/theory_black.Plo: No such file or directory +Makefile:977: .deps/theory/theory_uf_white.Plo: No such file or directory +Makefile:977: .deps/theory/theory_arith_white.Plo: No such file or directory +Makefile:977: .deps/expr/expr_public.Plo: No such file or directory +Makefile:977: .deps/expr/expr_manager_public.Plo: No such file or directory +Makefile:977: .deps/expr/node_white.Plo: No such file or directory +Makefile:977: .deps/expr/node_black.Plo: No such file or directory +Makefile:977: .deps/expr/kind_black.Plo: No such file or directory +Makefile:977: .deps/expr/node_builder_black.Plo: No such file or directory +Makefile:977: .deps/expr/node_manager_black.Plo: No such file or directory +Makefile:977: .deps/expr/node_manager_white.Plo: No such file or directory +Makefile:977: .deps/expr/attribute_white.Plo: No such file or directory +Makefile:977: .deps/expr/attribute_black.Plo: No such file or directory +Makefile:977: .deps/expr/declaration_scope_black.Plo: No such file or directory +Makefile:977: .deps/parser/parser_black.Plo: No such file or directory +Makefile:977: .deps/parser/parser_builder_black.Plo: No such file or directory +Makefile:977: .deps/prop/cnf_stream_black.Plo: No such file or directory +Makefile:977: .deps/context/context_black.Plo: No such file or directory +Makefile:977: .deps/context/context_white.Plo: No such file or directory +Makefile:977: .deps/context/context_mm_black.Plo: No such file or directory +Makefile:977: .deps/context/cdo_black.Plo: No such file or directory +Makefile:977: .deps/context/cdlist_black.Plo: No such file or directory +Makefile:977: .deps/context/cdmap_black.Plo: No such file or directory +Makefile:977: .deps/context/cdmap_white.Plo: No such file or directory +Makefile:977: .deps/util/assert_white.Plo: No such file or directory +Makefile:977: .deps/util/bitvector_black.Plo: No such file or directory +Makefile:977: .deps/util/configuration_black.Plo: No such file or directory +Makefile:977: .deps/util/output_black.Plo: No such file or directory +Makefile:977: .deps/util/exception_black.Plo: No such file or directory +Makefile:977: .deps/util/integer_black.Plo: No such file or directory +Makefile:977: .deps/util/integer_white.Plo: No such file or directory +Makefile:977: .deps/util/rational_black.Plo: No such file or directory +Makefile:977: .deps/util/rational_white.Plo: No such file or directory + GEN .deps/util/rational_white.Plo + GEN .deps/util/rational_black.Plo + GEN .deps/util/integer_white.Plo + GEN .deps/util/integer_black.Plo + GEN .deps/util/exception_black.Plo + GEN .deps/util/output_black.Plo + GEN .deps/util/configuration_black.Plo + GEN .deps/util/bitvector_black.Plo + GEN .deps/util/assert_white.Plo + GEN .deps/context/cdmap_white.Plo + GEN .deps/context/cdmap_black.Plo + GEN .deps/context/cdlist_black.Plo + GEN .deps/context/cdo_black.Plo + GEN .deps/context/context_mm_black.Plo + GEN .deps/context/context_white.Plo + GEN .deps/context/context_black.Plo + GEN .deps/prop/cnf_stream_black.Plo + GEN .deps/parser/parser_builder_black.Plo + GEN .deps/parser/parser_black.Plo + GEN .deps/expr/declaration_scope_black.Plo + GEN .deps/expr/attribute_black.Plo + GEN .deps/expr/attribute_white.Plo + GEN .deps/expr/node_manager_white.Plo + GEN .deps/expr/node_manager_black.Plo + GEN .deps/expr/node_builder_black.Plo + GEN .deps/expr/kind_black.Plo + GEN .deps/expr/node_black.Plo + GEN .deps/expr/node_white.Plo + GEN .deps/expr/expr_manager_public.Plo + GEN .deps/expr/expr_public.Plo + GEN .deps/theory/theory_arith_white.Plo + GEN .deps/theory/theory_uf_white.Plo + GEN .deps/theory/theory_black.Plo + GEN .deps/theory/theory_engine_white.Plo + GEN .deps/theory/shared_term_manager_black.Plo +make[5]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit' +make[5]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit' +make[5]: Nothing to be done for `all'. +make[5]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit' +Making all in system +make[5]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/system' +make[5]: Nothing to be done for `all'. +make[5]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/system' +Making all in regress +make[5]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/regress' +Making all in regress0 +make[6]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/regress/regress0' +Making all in . +make[7]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/regress/regress0' +make[7]: Nothing to be done for `all-am'. +make[7]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/regress/regress0' +Making all in precedence +make[7]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/regress/regress0/precedence' +make[7]: Nothing to be done for `all'. +make[7]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/regress/regress0/precedence' +Making all in uf +make[7]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/regress/regress0/uf' +make[7]: Nothing to be done for `all'. +make[7]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/regress/regress0/uf' +make[6]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/regress/regress0' +make[6]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/regress' +make[6]: Nothing to be done for `all-am'. +make[6]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/regress' +make[5]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/regress' +Making all in . +make[5]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test' +make[5]: Nothing to be done for `all-am'. +make[5]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test' +make[4]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test' +Making all in contrib +make[4]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/contrib' +make[4]: Nothing to be done for `all'. +make[4]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/contrib' +make[4]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition' +make[4]: Nothing to be done for `all-am'. +make[4]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition' +make[3]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition' +make[2]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition' +/bin/sh /home/mdeters/cvc4-smtcomp2010/config/install-sh -d "x86_64-unknown-linux-gnu/competition/usr/local/bin" "x86_64-unknown-linux-gnu/competition/usr/local/lib" +x86_64-unknown-linux-gnu/competition/libtool --mode=install install -v \ + x86_64-unknown-linux-gnu/competition/src/libcvc4.la \ + "/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/usr/local/lib" +libtool: install: install -v x86_64-unknown-linux-gnu/competition/src/.libs/libcvc4.lai /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/usr/local/lib/libcvc4.la +`x86_64-unknown-linux-gnu/competition/src/.libs/libcvc4.lai' -> `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/usr/local/lib/libcvc4.la' +libtool: install: install -v x86_64-unknown-linux-gnu/competition/src/.libs/libcvc4.a /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/usr/local/lib/libcvc4.a +`x86_64-unknown-linux-gnu/competition/src/.libs/libcvc4.a' -> `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/usr/local/lib/libcvc4.a' +libtool: install: chmod 644 /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/usr/local/lib/libcvc4.a +libtool: install: ranlib /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/usr/local/lib/libcvc4.a +libtool: install: warning: remember to run `libtool --finish /usr/local/lib' +x86_64-unknown-linux-gnu/competition/libtool --mode=install install -v \ + x86_64-unknown-linux-gnu/competition/src/parser/libcvc4parser.la \ + "/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/usr/local/lib" +libtool: install: install -v x86_64-unknown-linux-gnu/competition/src/parser/.libs/libcvc4parser.lai /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/usr/local/lib/libcvc4parser.la +`x86_64-unknown-linux-gnu/competition/src/parser/.libs/libcvc4parser.lai' -> `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/usr/local/lib/libcvc4parser.la' +libtool: install: install -v x86_64-unknown-linux-gnu/competition/src/parser/.libs/libcvc4parser.a /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/usr/local/lib/libcvc4parser.a +`x86_64-unknown-linux-gnu/competition/src/parser/.libs/libcvc4parser.a' -> `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/usr/local/lib/libcvc4parser.a' +libtool: install: chmod 644 /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/usr/local/lib/libcvc4parser.a +libtool: install: ranlib /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/usr/local/lib/libcvc4parser.a +libtool: install: warning: remember to run `libtool --finish /usr/local/lib/.' +/bin/sh /home/mdeters/cvc4-smtcomp2010/config/install-sh \ + x86_64-unknown-linux-gnu/competition/src/main/cvc4 \ + "/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/usr/local/bin" +test -e x86_64-unknown-linux-gnu/competition/lib || ln -sfv "/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/usr/local/lib" x86_64-unknown-linux-gnu/competition/lib +`x86_64-unknown-linux-gnu/competition/lib' -> `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/usr/local/lib' +test -e x86_64-unknown-linux-gnu/competition/bin || ln -sfv "/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/usr/local/bin" x86_64-unknown-linux-gnu/competition/bin +`x86_64-unknown-linux-gnu/competition/bin' -> `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/usr/local/bin' +/bin/sh /home/mdeters/cvc4-smtcomp2010/config/install-sh -d "./usr/local/bin" "./usr/local/lib" +x86_64-unknown-linux-gnu/competition/libtool --mode=install install -v x86_64-unknown-linux-gnu/competition/src/libcvc4.la "`pwd`/usr/local/lib" +libtool: install: install -v x86_64-unknown-linux-gnu/competition/src/.libs/libcvc4.lai /home/mdeters/cvc4-smtcomp2010/builds/usr/local/lib/libcvc4.la +`x86_64-unknown-linux-gnu/competition/src/.libs/libcvc4.lai' -> `/home/mdeters/cvc4-smtcomp2010/builds/usr/local/lib/libcvc4.la' +libtool: install: install -v x86_64-unknown-linux-gnu/competition/src/.libs/libcvc4.a /home/mdeters/cvc4-smtcomp2010/builds/usr/local/lib/libcvc4.a +`x86_64-unknown-linux-gnu/competition/src/.libs/libcvc4.a' -> `/home/mdeters/cvc4-smtcomp2010/builds/usr/local/lib/libcvc4.a' +libtool: install: chmod 644 /home/mdeters/cvc4-smtcomp2010/builds/usr/local/lib/libcvc4.a +libtool: install: ranlib /home/mdeters/cvc4-smtcomp2010/builds/usr/local/lib/libcvc4.a +libtool: install: warning: remember to run `libtool --finish /usr/local/lib' +x86_64-unknown-linux-gnu/competition/libtool --mode=install install -v x86_64-unknown-linux-gnu/competition/src/parser/libcvc4parser.la "`pwd`/usr/local/lib" +libtool: install: install -v x86_64-unknown-linux-gnu/competition/src/parser/.libs/libcvc4parser.lai /home/mdeters/cvc4-smtcomp2010/builds/usr/local/lib/libcvc4parser.la +`x86_64-unknown-linux-gnu/competition/src/parser/.libs/libcvc4parser.lai' -> `/home/mdeters/cvc4-smtcomp2010/builds/usr/local/lib/libcvc4parser.la' +libtool: install: install -v x86_64-unknown-linux-gnu/competition/src/parser/.libs/libcvc4parser.a /home/mdeters/cvc4-smtcomp2010/builds/usr/local/lib/libcvc4parser.a +`x86_64-unknown-linux-gnu/competition/src/parser/.libs/libcvc4parser.a' -> `/home/mdeters/cvc4-smtcomp2010/builds/usr/local/lib/libcvc4parser.a' +libtool: install: chmod 644 /home/mdeters/cvc4-smtcomp2010/builds/usr/local/lib/libcvc4parser.a +libtool: install: ranlib /home/mdeters/cvc4-smtcomp2010/builds/usr/local/lib/libcvc4parser.a +libtool: install: warning: remember to run `libtool --finish /usr/local/lib/.' +/bin/sh /home/mdeters/cvc4-smtcomp2010/config/install-sh x86_64-unknown-linux-gnu/competition/src/main/cvc4 "`pwd`/usr/local/bin" +test -e lib || ln -sfv "./usr/local/lib" lib +`lib' -> `./usr/local/lib' +test -e bin || ln -sfv "./usr/local/bin" bin +`bin' -> `./usr/local/bin' +make[1]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds' ++ strip builds/bin/cvc4 ++ make -k check +cd builds +make check +make[1]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds' +(cd x86_64-unknown-linux-gnu/competition && make check) +make[2]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition' +Making check in src +make[3]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src' +Making check in expr +make[4]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/expr' +make check-am +make[5]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/expr' +make[5]: Nothing to be done for `check-am'. +make[5]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/expr' +make[4]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/expr' +Making check in util +make[4]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/util' +make check-am +make[5]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/util' +make[5]: Nothing to be done for `check-am'. +make[5]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/util' +make[4]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/util' +Making check in context +make[4]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/context' +make[4]: Nothing to be done for `check'. +make[4]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/context' +Making check in theory +make[4]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/theory' +make check-recursive +make[5]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/theory' +Making check in builtin +make[6]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/theory/builtin' +make[6]: Nothing to be done for `check'. +make[6]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/theory/builtin' +Making check in booleans +make[6]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/theory/booleans' +make[6]: Nothing to be done for `check'. +make[6]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/theory/booleans' +Making check in uf +make[6]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/theory/uf' +make[6]: Nothing to be done for `check'. +make[6]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/theory/uf' +Making check in arith +make[6]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/theory/arith' +make[6]: Nothing to be done for `check'. +make[6]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/theory/arith' +Making check in arrays +make[6]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/theory/arrays' +make[6]: Nothing to be done for `check'. +make[6]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/theory/arrays' +Making check in bv +make[6]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/theory/bv' +make[6]: Nothing to be done for `check'. +make[6]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/theory/bv' +make[6]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/theory' +make[6]: Nothing to be done for `check-am'. +make[6]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/theory' +make[5]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/theory' +make[4]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/theory' +Making check in prop +make[4]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/prop' +Making check in minisat +make[5]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/prop/minisat' +make[5]: Nothing to be done for `check'. +make[5]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/prop/minisat' +make[5]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/prop' +make[5]: Nothing to be done for `check-am'. +make[5]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/prop' +make[4]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/prop' +Making check in smt +make[4]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/smt' +make[4]: Nothing to be done for `check'. +make[4]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/smt' +Making check in . +make[4]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src' +make[4]: Nothing to be done for `check-am'. +make[4]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src' +Making check in parser +make[4]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/parser' +Making check in smt +make[5]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/parser/smt' +make check-am +make[6]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/parser/smt' +make[6]: Nothing to be done for `check-am'. +make[6]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/parser/smt' +make[5]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/parser/smt' +Making check in smt2 +make[5]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/parser/smt2' +make check-am +make[6]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/parser/smt2' +make[6]: Nothing to be done for `check-am'. +make[6]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/parser/smt2' +make[5]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/parser/smt2' +Making check in cvc +make[5]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/parser/cvc' +make check-am +make[6]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/parser/cvc' +make[6]: Nothing to be done for `check-am'. +make[6]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/parser/cvc' +make[5]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/parser/cvc' +make[5]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/parser' +make[5]: Nothing to be done for `check-am'. +make[5]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/parser' +make[4]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/parser' +Making check in main +make[4]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/main' +make[4]: Nothing to be done for `check'. +make[4]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/main' +make[3]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src' +Making check in test +make[3]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test' +Making check in unit +make[4]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit' +make check-TESTS +make[5]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit' + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit/theory/shared_term_manager_black.cpp + CXX theory/shared_term_manager_black.lo + CXXLD theory/shared_term_manager_black + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit/theory/theory_engine_white.cpp + CXX theory/theory_engine_white.lo + CXXLD theory/theory_engine_white + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit/theory/theory_black.cpp + CXX theory/theory_black.lo + CXXLD theory/theory_black + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit/theory/theory_uf_white.cpp + CXX theory/theory_uf_white.lo + CXXLD theory/theory_uf_white + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit/theory/theory_arith_white.cpp + CXX theory/theory_arith_white.lo + CXXLD theory/theory_arith_white + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit/expr/expr_public.cpp + CXX expr/expr_public.lo + CXXLD expr/expr_public + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit/expr/expr_manager_public.cpp + CXX expr/expr_manager_public.lo + CXXLD expr/expr_manager_public + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit/expr/node_white.cpp + CXX expr/node_white.lo + CXXLD expr/node_white + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit/expr/node_black.cpp + CXX expr/node_black.lo + CXXLD expr/node_black + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit/expr/kind_black.cpp + CXX expr/kind_black.lo + CXXLD expr/kind_black + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit/expr/node_builder_black.cpp + CXX expr/node_builder_black.lo + CXXLD expr/node_builder_black + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit/expr/node_manager_black.cpp + CXX expr/node_manager_black.lo + CXXLD expr/node_manager_black + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit/expr/node_manager_white.cpp + CXX expr/node_manager_white.lo + CXXLD expr/node_manager_white + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit/expr/attribute_white.cpp + CXX expr/attribute_white.lo + CXXLD expr/attribute_white + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit/expr/attribute_black.cpp + CXX expr/attribute_black.lo + CXXLD expr/attribute_black + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit/expr/declaration_scope_black.cpp + CXX expr/declaration_scope_black.lo + CXXLD expr/declaration_scope_black + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit/parser/parser_black.cpp + CXX parser/parser_black.lo + CXXLD parser/parser_black + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit/parser/parser_builder_black.cpp + CXX parser/parser_builder_black.lo + CXXLD parser/parser_builder_black + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit/prop/cnf_stream_black.cpp + CXX prop/cnf_stream_black.lo + CXXLD prop/cnf_stream_black + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit/context/context_black.cpp + CXX context/context_black.lo + CXXLD context/context_black + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit/context/context_white.cpp + CXX context/context_white.lo + CXXLD context/context_white + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit/context/context_mm_black.cpp + CXX context/context_mm_black.lo + CXXLD context/context_mm_black + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit/context/cdo_black.cpp + CXX context/cdo_black.lo + CXXLD context/cdo_black + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit/context/cdlist_black.cpp + CXX context/cdlist_black.lo + CXXLD context/cdlist_black + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit/context/cdmap_black.cpp + CXX context/cdmap_black.lo + CXXLD context/cdmap_black + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit/context/cdmap_white.cpp + CXX context/cdmap_white.lo + CXXLD context/cdmap_white + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit/util/assert_white.cpp + CXX util/assert_white.lo + CXXLD util/assert_white + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit/util/bitvector_black.cpp + CXX util/bitvector_black.lo + CXXLD util/bitvector_black + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit/util/configuration_black.cpp + CXX util/configuration_black.lo + CXXLD util/configuration_black + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit/util/output_black.cpp + CXX util/output_black.lo + CXXLD util/output_black + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit/util/exception_black.cpp + CXX util/exception_black.lo + CXXLD util/exception_black + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit/util/integer_black.cpp + CXX util/integer_black.lo + CXXLD util/integer_black + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit/util/integer_white.cpp + CXX util/integer_white.lo + CXXLD util/integer_white + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit/util/rational_black.cpp + CXX util/rational_black.lo + CXXLD util/rational_black + GEN /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit/util/rational_white.cpp + CXX util/rational_white.lo + CXXLD util/rational_white +make[6]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit' +PASS: theory/shared_term_manager_black +PASS: theory/theory_engine_white +PASS: theory/theory_black +PASS: theory/theory_uf_white +/bin/bash: line 1: 29784 Segmentation fault "$tst" > theory/theory_arith_white.log-t 2>&1 +FAIL: theory/theory_arith_white +PASS: expr/expr_public +PASS: expr/expr_manager_public +PASS: expr/node_white +PASS: expr/node_black +PASS: expr/kind_black +PASS: expr/node_builder_black +PASS: expr/node_manager_black +PASS: expr/node_manager_white +PASS: expr/attribute_white +PASS: expr/attribute_black +PASS: expr/declaration_scope_black +PASS: parser/parser_black +PASS: parser/parser_builder_black +PASS: prop/cnf_stream_black +PASS: context/context_black +PASS: context/context_white +PASS: context/context_mm_black +PASS: context/cdo_black +PASS: context/cdlist_black +PASS: context/cdmap_black +PASS: context/cdmap_white +PASS: util/assert_white +PASS: util/bitvector_black +PASS: util/configuration_black +PASS: util/output_black +PASS: util/exception_black +PASS: util/integer_black +PASS: util/integer_white +PASS: util/rational_black +PASS: util/rational_white +====================================================== + cvc4 1.0a0-smtcomp2010: test/unit/test-suite.log +====================================================== + +1 of 35 tests failed. + +.. contents:: :depth: 2 + + +FAIL: theory/theory_arith_white (exit: 139) +=========================================== + +Running 8 tests. +In TheoryArithWhite::testAssertEqualityEagerSplit: +/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/unit/theory/theory_arith_white.h:146: Error: Test failed: Exception thrown from test +. +In TheoryArithWhite::testBasicConflict: +/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/unit/theory/theory_arith_white.h:178: Error: Test failed: Exception thrown from test +In TheoryArithWhite::testBasicPropagate: +/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/unit/theory/theory_arith_white.h:206: Error: Test failed: Exception thrown from test +In TheoryArithWhite::testTPLt1: +/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/unit/theory/theory_arith_white.h:257: Error: Expected (d_outputChannel.getNumCalls() == 2u), found (3 != 2) +/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/unit/theory/theory_arith_white.h:258: Error: Expected (d_outputChannel.getIthCallType(0) == PROPAGATE), found ({ 02 00 00 00 } != { 01 00 00 00 }) +/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/unit/theory/theory_arith_white.h:259: Error: Expected (d_outputChannel.getIthCallType(1) == EXPLANATION), found ({ 02 00 00 00 } != { 04 00 00 00 }) +/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/unit/theory/theory_arith_white.h:260: Error: Expected (d_outputChannel.getIthNode(0) == leq1), found ({ 70 F5 B6 01 00 00 00 00 } != { D0 EF B6 01 00 00 00 00 }) +/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/unit/theory/theory_arith_white.h:261: Error: Expected (d_outputChannel.getIthNode(1) == rLt1), found ({ A0 F6 B6 01 00 00 00 00 } != { 50 F0 B6 01 00 00 00 00 }) +In TheoryArithWhite::testTPLeq0: +/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/unit/theory/theory_arith_white.h:291: Error: Expected (d_outputChannel.getNumCalls() == 4u), found (3 != 4) +/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/unit/theory/theory_arith_white.h:292: Error: Expected (d_outputChannel.getIthCallType(0) == PROPAGATE), found ({ 02 00 00 00 } != { 01 00 00 00 }) +/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/unit/theory/theory_arith_white.h:293: Error: Expected (d_outputChannel.getIthCallType(1) == PROPAGATE), found ({ 02 00 00 00 } != { 01 00 00 00 }) +/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/unit/theory/theory_arith_white.h:294: Error: Expected (d_outputChannel.getIthCallType(2) == EXPLANATION), found ({ 02 00 00 00 } != { 04 00 00 00 }) +/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/unit/theory/theory_arith_white.h:295: Error: Expected (d_outputChannel.getIthCallType(3) == EXPLANATION), found ({ 00 00 00 00 } != { 04 00 00 00 }) +/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/unit/theory/theory_arith_white.h:297: Error: Expected (d_outputChannel.getIthNode(0) == rLt1), found ({ 90 D2 B6 01 00 00 00 00 } != { 70 CD B6 01 00 00 00 00 }) +/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/unit/theory/theory_arith_white.h:298: Error: Expected (d_outputChannel.getIthNode(1) == rLeq1), found ({ 90 D3 B6 01 00 00 00 00 } != { F0 CC B6 01 00 00 00 00 }) +/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/unit/theory/theory_arith_white.h:301: Error: Expected (d_outputChannel.getIthNode(2) == rLeq0), found ({ 30 D4 B6 01 00 00 00 00 } != { B0 CC B6 01 00 00 00 00 }) +============================ +1 of 35 tests failed +See test/unit/test-suite.log +============================ +make[6]: *** [test-suite.log] Error 1 +make[6]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit' +make[5]: *** [check-TESTS] Error 2 +make[5]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit' +make[4]: *** [check-am] Error 2 +make[4]: Target `check' not remade because of errors. +make[4]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit' +Making check in system +make[4]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/system' +make check-TESTS +make[5]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/system' +make[6]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/system' +================== +All 0 tests passed +================== +make[6]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/system' +make[5]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/system' +make[4]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/system' +Making check in regress +make[4]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/regress' +Making check in regress0 +make[5]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/regress/regress0' +Making check in . +make[6]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/regress/regress0' +make check-TESTS +make[7]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/regress/regress0' +make[8]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/regress/regress0' +PASS: distinct.smt +PASS: flet.smt +PASS: flet2.smt +PASS: fuzz_1.smt +PASS: fuzz_3.smt +PASS: ineq_basic.smt +PASS: ineq_slack.smt +PASS: ite_real_int_type.smt +PASS: ite_real_valid.smt +FAIL: let.smt +FAIL: let2.smt +PASS: simple.smt +PASS: simple2.smt +PASS: simple-lra.smt +PASS: simple-rdl.smt +FAIL: simple-uf.smt +PASS: ite2.smt2 +FAIL: ite3.smt2 +FAIL: ite4.smt2 +PASS: simple-lra.smt2 +PASS: simple-rdl.smt2 +FAIL: simple-uf.smt2 +PASS: boolean-prec.cvc +PASS: bug167.smt +PASS: bug169.smt +PASS: hole6.cvc +PASS: ite.cvc +PASS: logops.01.cvc +PASS: logops.02.cvc +PASS: logops.03.cvc +PASS: logops.04.cvc +PASS: logops.05.cvc +PASS: simple.cvc +PASS: smallcnf.cvc +PASS: test11.cvc +PASS: test9.cvc +PASS: uf20-03.cvc +PASS: wiki.01.cvc +PASS: wiki.02.cvc +PASS: wiki.03.cvc +PASS: wiki.04.cvc +PASS: wiki.05.cvc +PASS: wiki.06.cvc +PASS: wiki.07.cvc +PASS: wiki.08.cvc +PASS: wiki.09.cvc +PASS: wiki.10.cvc +PASS: wiki.11.cvc +PASS: wiki.12.cvc +PASS: wiki.13.cvc +PASS: wiki.14.cvc +PASS: wiki.15.cvc +PASS: wiki.16.cvc +PASS: wiki.17.cvc +PASS: wiki.18.cvc +PASS: wiki.19.cvc +PASS: wiki.20.cvc +PASS: wiki.21.cvc +PASS: bug2.smt +PASS: bug32.cvc +FAIL: bug49.smt +PASS: bug161.smt +PASS: bug164.smt +PASS: bug168.smt +================================================================== + cvc4 1.0a0-smtcomp2010: test/regress/regress0/test-suite.log +================================================================== + +7 of 65 tests failed. + +.. contents:: :depth: 2 + + +FAIL: let.smt (exit: 1) +======================= + +running /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/main/cvc4 let.smt from /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0 +run_regression: error: differences between expected and actual output on stdout +--- /tmp/cvc4_expect_stdout.qaGMU5SQRv 2010-07-10 18:02:02.000000000 -0400 ++++ /tmp/cvc4_stdout.Be72nSmTEC 2010-07-10 18:02:02.000000000 -0400 +@@ -1 +0,0 @@ +-UNSAT +run_regression: error: differences between expected and actual output on stderr +--- /tmp/cvc4_expect_stderr.dHC3woX6qN 2010-07-10 18:02:02.000000000 -0400 ++++ /tmp/cvc4_stderr.RX7hXqny6t 2010-07-10 18:02:02.000000000 -0400 +@@ -0,0 +1,2 @@ ++CVC4 suffered a segfault. ++/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/../run_regression: line 137: 30700 Aborted "$cvc4full" --segv-nospin `basename "$benchmark"` +run_regression: error: expected exit status `20' but got `134' + +FAIL: let2.smt (exit: 1) +======================== + +running /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/main/cvc4 let2.smt from /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0 +run_regression: error: differences between expected and actual output on stdout +--- /tmp/cvc4_expect_stdout.TyFw4w4zHJ 2010-07-10 18:02:02.000000000 -0400 ++++ /tmp/cvc4_stdout.PqXMUS2tDc 2010-07-10 18:02:02.000000000 -0400 +@@ -1 +0,0 @@ +-SAT +run_regression: error: differences between expected and actual output on stderr +--- /tmp/cvc4_expect_stderr.XDuj4T5zq2 2010-07-10 18:02:02.000000000 -0400 ++++ /tmp/cvc4_stderr.1ppBGK3V02 2010-07-10 18:02:02.000000000 -0400 +@@ -0,0 +1,2 @@ ++CVC4 suffered a segfault. ++/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/../run_regression: line 137: 30740 Aborted "$cvc4full" --segv-nospin `basename "$benchmark"` +run_regression: error: expected exit status `10' but got `134' + +FAIL: simple-uf.smt (exit: 1) +============================= + +running /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/main/cvc4 simple-uf.smt from /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0 +run_regression: error: differences between expected and actual output on stdout +--- /tmp/cvc4_expect_stdout.Dm6Roxudev 2010-07-10 18:02:03.000000000 -0400 ++++ /tmp/cvc4_stdout.zhB2myxF0u 2010-07-10 18:02:03.000000000 -0400 +@@ -1 +0,0 @@ +-UNSAT +run_regression: error: differences between expected and actual output on stderr +--- /tmp/cvc4_expect_stderr.A1pJpYrMwJ 2010-07-10 18:02:03.000000000 -0400 ++++ /tmp/cvc4_stderr.JNkn5YcHkA 2010-07-10 18:02:03.000000000 -0400 +@@ -0,0 +1,2 @@ ++CVC4 suffered a segfault. ++/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/../run_regression: line 137: 30944 Aborted "$cvc4full" --segv-nospin `basename "$benchmark"` +run_regression: error: expected exit status `20' but got `134' + +FAIL: ite3.smt2 (exit: 1) +========================= + +running /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/main/cvc4 ite3.smt2 from /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0 +run_regression: error: differences between expected and actual output on stdout +--- /tmp/cvc4_expect_stdout.pQEGvwPZHS 2010-07-10 18:02:03.000000000 -0400 ++++ /tmp/cvc4_stdout.JhIEHDSW4o 2010-07-10 18:02:03.000000000 -0400 +@@ -1 +0,0 @@ +-UNSAT +run_regression: error: differences between expected and actual output on stderr +--- /tmp/cvc4_expect_stderr.37f85TpleS 2010-07-10 18:02:03.000000000 -0400 ++++ /tmp/cvc4_stderr.fhEb3lGzI4 2010-07-10 18:02:03.000000000 -0400 +@@ -0,0 +1,2 @@ ++CVC4 suffered a segfault. ++/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/../run_regression: line 137: 31027 Aborted "$cvc4full" --segv-nospin `basename "$benchmark"` +run_regression: error: expected exit status `20' but got `134' + +FAIL: ite4.smt2 (exit: 1) +========================= + +running /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/main/cvc4 ite4.smt2 from /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0 +run_regression: error: differences between expected and actual output on stdout +--- /tmp/cvc4_expect_stdout.zrJ4s4QTxI 2010-07-10 18:02:03.000000000 -0400 ++++ /tmp/cvc4_stdout.OMwAI4D2lW 2010-07-10 18:02:03.000000000 -0400 +@@ -1 +0,0 @@ +-SAT +run_regression: error: differences between expected and actual output on stderr +--- /tmp/cvc4_expect_stderr.s3WiyoMb58 2010-07-10 18:02:03.000000000 -0400 ++++ /tmp/cvc4_stderr.0RjKxX46lB 2010-07-10 18:02:03.000000000 -0400 +@@ -0,0 +1,2 @@ ++CVC4 suffered a segfault. ++/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/../run_regression: line 137: 31068 Aborted "$cvc4full" --segv-nospin `basename "$benchmark"` +run_regression: error: expected exit status `10' but got `134' + +FAIL: simple-uf.smt2 (exit: 1) +============================== + +running /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/main/cvc4 simple-uf.smt2 from /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0 +run_regression: error: differences between expected and actual output on stdout +--- /tmp/cvc4_expect_stdout.vR2X7rVscA 2010-07-10 18:02:03.000000000 -0400 ++++ /tmp/cvc4_stdout.87UWkhOJm8 2010-07-10 18:02:03.000000000 -0400 +@@ -1 +0,0 @@ +-UNSAT +run_regression: error: differences between expected and actual output on stderr +--- /tmp/cvc4_expect_stderr.ljxn6x1giv 2010-07-10 18:02:03.000000000 -0400 ++++ /tmp/cvc4_stderr.vhBR9JXue0 2010-07-10 18:02:03.000000000 -0400 +@@ -0,0 +1,2 @@ ++CVC4 suffered a segfault. ++/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/../run_regression: line 137: 31194 Aborted "$cvc4full" --segv-nospin `basename "$benchmark"` +run_regression: error: expected exit status `20' but got `134' + +FAIL: bug49.smt (exit: 1) +========================= + +running /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/main/cvc4 bug49.smt from /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0 +run_regression: error: differences between expected and actual output on stdout +--- /tmp/cvc4_expect_stdout.7cxIIG0OM8 2010-07-10 18:02:07.000000000 -0400 ++++ /tmp/cvc4_stdout.TxxPtPk4FD 2010-07-10 18:02:07.000000000 -0400 +@@ -1 +0,0 @@ +-SAT +run_regression: error: differences between expected and actual output on stderr +--- /tmp/cvc4_expect_stderr.Ze7ydMSAVq 2010-07-10 18:02:07.000000000 -0400 ++++ /tmp/cvc4_stderr.VaxdRh0he7 2010-07-10 18:02:07.000000000 -0400 +@@ -0,0 +1,2 @@ ++CVC4 suffered a segfault. ++/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/../run_regression: line 137: 605 Aborted "$cvc4full" --segv-nospin `basename "$benchmark"` +run_regression: error: expected exit status `10' but got `134' +======================================== +7 of 65 tests failed +See test/regress/regress0/test-suite.log +======================================== +make[8]: *** [test-suite.log] Error 1 +make[8]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/regress/regress0' +make[7]: *** [check-TESTS] Error 2 +make[7]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/regress/regress0' +make[6]: *** [check-am] Error 2 +make[6]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/regress/regress0' +Making check in precedence +make[6]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/regress/regress0/precedence' +make check-TESTS +make[7]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/regress/regress0/precedence' +make[8]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/regress/regress0/precedence' +PASS: and-xor.cvc +PASS: and-not.cvc +PASS: bool-cmp.cvc +PASS: cmp-plus.cvc +PASS: eq-fun.cvc +PASS: iff-assoc.cvc +PASS: iff-implies.cvc +PASS: implies-assoc.cvc +PASS: implies-iff.cvc +PASS: implies-or.cvc +PASS: not-and.cvc +PASS: not-eq.cvc +PASS: plus-mult.cvc +PASS: or-implies.cvc +PASS: or-xor.cvc +PASS: xor-or.cvc +PASS: xor-and.cvc +PASS: xor-assoc.cvc +=================== +All 18 tests passed +=================== +make[8]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/regress/regress0/precedence' +make[7]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/regress/regress0/precedence' +make[6]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/regress/regress0/precedence' +Making check in uf +make[6]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/regress/regress0/uf' +make check-TESTS +make[7]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/regress/regress0/uf' +make[8]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/regress/regress0/uf' +FAIL: euf_simp01.smt +FAIL: euf_simp02.smt +FAIL: euf_simp03.smt +FAIL: euf_simp04.smt +FAIL: euf_simp05.smt +FAIL: euf_simp06.smt +FAIL: euf_simp08.smt +FAIL: euf_simp09.smt +FAIL: euf_simp10.smt +FAIL: euf_simp11.smt +FAIL: euf_simp12.smt +FAIL: euf_simp13.smt +PASS: dead_dnd002.smt +FAIL: iso_brn001.smt +FAIL: SEQ032_size2.smt +FAIL: simple.01.cvc +FAIL: simple.02.cvc +FAIL: simple.03.cvc +FAIL: simple.04.cvc +===================================================================== + cvc4 1.0a0-smtcomp2010: test/regress/regress0/uf/test-suite.log +===================================================================== + +18 of 19 tests failed. + +.. contents:: :depth: 2 + + +FAIL: euf_simp01.smt (exit: 1) +============================== + +running /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/main/cvc4 euf_simp01.smt from /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/uf +run_regression: error: differences between expected and actual output on stdout +--- /tmp/cvc4_expect_stdout.ww4MAdgraD 2010-07-10 18:02:10.000000000 -0400 ++++ /tmp/cvc4_stdout.F8jibClear 2010-07-10 18:02:10.000000000 -0400 +@@ -1 +0,0 @@ +-SAT +run_regression: error: differences between expected and actual output on stderr +--- /tmp/cvc4_expect_stderr.eK4Xh5mB8u 2010-07-10 18:02:10.000000000 -0400 ++++ /tmp/cvc4_stderr.I6bcct7oGo 2010-07-10 18:02:10.000000000 -0400 +@@ -0,0 +1,2 @@ ++CVC4 suffered a segfault. ++/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/uf/../../run_regression: line 137: 1842 Aborted "$cvc4full" --segv-nospin `basename "$benchmark"` +run_regression: error: expected exit status `10' but got `134' + +FAIL: euf_simp02.smt (exit: 1) +============================== + +running /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/main/cvc4 euf_simp02.smt from /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/uf +run_regression: error: differences between expected and actual output on stdout +--- /tmp/cvc4_expect_stdout.96bCdTdtKv 2010-07-10 18:02:10.000000000 -0400 ++++ /tmp/cvc4_stdout.s4LW9ukTBY 2010-07-10 18:02:10.000000000 -0400 +@@ -1 +0,0 @@ +-UNSAT +run_regression: error: differences between expected and actual output on stderr +--- /tmp/cvc4_expect_stderr.BamwY4NjOV 2010-07-10 18:02:10.000000000 -0400 ++++ /tmp/cvc4_stderr.I9wC0IVIpT 2010-07-10 18:02:10.000000000 -0400 +@@ -0,0 +1,2 @@ ++CVC4 suffered a segfault. ++/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/uf/../../run_regression: line 137: 1883 Aborted "$cvc4full" --segv-nospin `basename "$benchmark"` +run_regression: error: expected exit status `20' but got `134' + +FAIL: euf_simp03.smt (exit: 1) +============================== + +running /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/main/cvc4 euf_simp03.smt from /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/uf +run_regression: error: differences between expected and actual output on stdout +--- /tmp/cvc4_expect_stdout.vSNXaLQ2qr 2010-07-10 18:02:10.000000000 -0400 ++++ /tmp/cvc4_stdout.xTPyXict3i 2010-07-10 18:02:10.000000000 -0400 +@@ -1 +0,0 @@ +-UNSAT +run_regression: error: differences between expected and actual output on stderr +--- /tmp/cvc4_expect_stderr.3nWzlp85zy 2010-07-10 18:02:10.000000000 -0400 ++++ /tmp/cvc4_stderr.srNyVKx3pf 2010-07-10 18:02:10.000000000 -0400 +@@ -0,0 +1,2 @@ ++CVC4 suffered a segfault. ++/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/uf/../../run_regression: line 137: 1924 Aborted "$cvc4full" --segv-nospin `basename "$benchmark"` +run_regression: error: expected exit status `20' but got `134' + +FAIL: euf_simp04.smt (exit: 1) +============================== + +running /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/main/cvc4 euf_simp04.smt from /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/uf +run_regression: error: differences between expected and actual output on stdout +--- /tmp/cvc4_expect_stdout.DYEXgdIsIP 2010-07-10 18:02:10.000000000 -0400 ++++ /tmp/cvc4_stdout.QP3a5ue8Dh 2010-07-10 18:02:10.000000000 -0400 +@@ -1 +0,0 @@ +-UNSAT +run_regression: error: differences between expected and actual output on stderr +--- /tmp/cvc4_expect_stderr.QwD10Rndde 2010-07-10 18:02:10.000000000 -0400 ++++ /tmp/cvc4_stderr.5zuDyPJeQr 2010-07-10 18:02:10.000000000 -0400 +@@ -0,0 +1,2 @@ ++CVC4 suffered a segfault. ++/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/uf/../../run_regression: line 137: 1965 Aborted "$cvc4full" --segv-nospin `basename "$benchmark"` +run_regression: error: expected exit status `20' but got `134' + +FAIL: euf_simp05.smt (exit: 1) +============================== + +running /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/main/cvc4 euf_simp05.smt from /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/uf +run_regression: error: differences between expected and actual output on stdout +--- /tmp/cvc4_expect_stdout.z9iDzgFkMn 2010-07-10 18:02:10.000000000 -0400 ++++ /tmp/cvc4_stdout.UfJ9aqmVcK 2010-07-10 18:02:10.000000000 -0400 +@@ -1 +0,0 @@ +-UNSAT +run_regression: error: differences between expected and actual output on stderr +--- /tmp/cvc4_expect_stderr.ZAU5hLyi6D 2010-07-10 18:02:10.000000000 -0400 ++++ /tmp/cvc4_stderr.sHJMXMyVEq 2010-07-10 18:02:10.000000000 -0400 +@@ -0,0 +1,2 @@ ++CVC4 suffered a segfault. ++/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/uf/../../run_regression: line 137: 2006 Aborted "$cvc4full" --segv-nospin `basename "$benchmark"` +run_regression: error: expected exit status `20' but got `134' + +FAIL: euf_simp06.smt (exit: 1) +============================== + +running /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/main/cvc4 euf_simp06.smt from /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/uf +run_regression: error: differences between expected and actual output on stdout +--- /tmp/cvc4_expect_stdout.S0TMViSyPj 2010-07-10 18:02:10.000000000 -0400 ++++ /tmp/cvc4_stdout.ZWjjVMJwqY 2010-07-10 18:02:10.000000000 -0400 +@@ -1 +0,0 @@ +-UNSAT +run_regression: error: differences between expected and actual output on stderr +--- /tmp/cvc4_expect_stderr.oXvs8UEv0L 2010-07-10 18:02:10.000000000 -0400 ++++ /tmp/cvc4_stderr.33fOc8dMCk 2010-07-10 18:02:10.000000000 -0400 +@@ -0,0 +1,2 @@ ++CVC4 suffered a segfault. ++/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/uf/../../run_regression: line 137: 2047 Aborted "$cvc4full" --segv-nospin `basename "$benchmark"` +run_regression: error: expected exit status `20' but got `134' + +FAIL: euf_simp08.smt (exit: 1) +============================== + +running /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/main/cvc4 euf_simp08.smt from /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/uf +run_regression: error: differences between expected and actual output on stdout +--- /tmp/cvc4_expect_stdout.iSeIDzZQE6 2010-07-10 18:02:11.000000000 -0400 ++++ /tmp/cvc4_stdout.tzrKY7eJ4O 2010-07-10 18:02:11.000000000 -0400 +@@ -1 +0,0 @@ +-UNSAT +run_regression: error: differences between expected and actual output on stderr +--- /tmp/cvc4_expect_stderr.Y9ysjbouaN 2010-07-10 18:02:11.000000000 -0400 ++++ /tmp/cvc4_stderr.hauuegzPsL 2010-07-10 18:02:11.000000000 -0400 +@@ -0,0 +1,2 @@ ++CVC4 suffered a segfault. ++/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/uf/../../run_regression: line 137: 2088 Aborted "$cvc4full" --segv-nospin `basename "$benchmark"` +run_regression: error: expected exit status `20' but got `134' + +FAIL: euf_simp09.smt (exit: 1) +============================== + +running /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/main/cvc4 euf_simp09.smt from /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/uf +run_regression: error: differences between expected and actual output on stdout +--- /tmp/cvc4_expect_stdout.AKx7rgFf5k 2010-07-10 18:02:11.000000000 -0400 ++++ /tmp/cvc4_stdout.PXQUTxvnJI 2010-07-10 18:02:11.000000000 -0400 +@@ -1 +0,0 @@ +-UNSAT +run_regression: error: differences between expected and actual output on stderr +--- /tmp/cvc4_expect_stderr.ct8elNn54W 2010-07-10 18:02:11.000000000 -0400 ++++ /tmp/cvc4_stderr.18kvOxjxy3 2010-07-10 18:02:11.000000000 -0400 +@@ -0,0 +1,2 @@ ++CVC4 suffered a segfault. ++/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/uf/../../run_regression: line 137: 2129 Aborted "$cvc4full" --segv-nospin `basename "$benchmark"` +run_regression: error: expected exit status `20' but got `134' + +FAIL: euf_simp10.smt (exit: 1) +============================== + +running /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/main/cvc4 euf_simp10.smt from /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/uf +run_regression: error: differences between expected and actual output on stdout +--- /tmp/cvc4_expect_stdout.5VIwk3wEgN 2010-07-10 18:02:11.000000000 -0400 ++++ /tmp/cvc4_stdout.jfoTN5nKxm 2010-07-10 18:02:11.000000000 -0400 +@@ -1 +0,0 @@ +-UNSAT +run_regression: error: differences between expected and actual output on stderr +--- /tmp/cvc4_expect_stderr.sXjiiPlGzo 2010-07-10 18:02:11.000000000 -0400 ++++ /tmp/cvc4_stderr.gsyCfgq7v1 2010-07-10 18:02:11.000000000 -0400 +@@ -0,0 +1,2 @@ ++CVC4 suffered a segfault. ++/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/uf/../../run_regression: line 137: 2170 Aborted "$cvc4full" --segv-nospin `basename "$benchmark"` +run_regression: error: expected exit status `20' but got `134' + +FAIL: euf_simp11.smt (exit: 1) +============================== + +running /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/main/cvc4 euf_simp11.smt from /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/uf +run_regression: error: differences between expected and actual output on stdout +--- /tmp/cvc4_expect_stdout.NPScHJ4RFs 2010-07-10 18:02:11.000000000 -0400 ++++ /tmp/cvc4_stdout.aVhavRoM9y 2010-07-10 18:02:11.000000000 -0400 +@@ -1 +0,0 @@ +-UNSAT +run_regression: error: differences between expected and actual output on stderr +--- /tmp/cvc4_expect_stderr.tF0UtWWypS 2010-07-10 18:02:11.000000000 -0400 ++++ /tmp/cvc4_stderr.Dojy3DKgU6 2010-07-10 18:02:11.000000000 -0400 +@@ -0,0 +1,2 @@ ++CVC4 suffered a segfault. ++/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/uf/../../run_regression: line 137: 2211 Aborted "$cvc4full" --segv-nospin `basename "$benchmark"` +run_regression: error: expected exit status `20' but got `134' + +FAIL: euf_simp12.smt (exit: 1) +============================== + +running /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/main/cvc4 euf_simp12.smt from /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/uf +run_regression: error: differences between expected and actual output on stdout +--- /tmp/cvc4_expect_stdout.YeCJ3TReqV 2010-07-10 18:02:11.000000000 -0400 ++++ /tmp/cvc4_stdout.ODwUa3hrN7 2010-07-10 18:02:11.000000000 -0400 +@@ -1 +0,0 @@ +-UNSAT +run_regression: error: differences between expected and actual output on stderr +--- /tmp/cvc4_expect_stderr.A9zpaV9481 2010-07-10 18:02:11.000000000 -0400 ++++ /tmp/cvc4_stderr.Y2ovO70nL8 2010-07-10 18:02:11.000000000 -0400 +@@ -0,0 +1,2 @@ ++CVC4 suffered a segfault. ++/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/uf/../../run_regression: line 137: 2252 Aborted "$cvc4full" --segv-nospin `basename "$benchmark"` +run_regression: error: expected exit status `20' but got `134' + +FAIL: euf_simp13.smt (exit: 1) +============================== + +running /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/main/cvc4 euf_simp13.smt from /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/uf +run_regression: error: differences between expected and actual output on stdout +--- /tmp/cvc4_expect_stdout.ybO4PjgUBr 2010-07-10 18:02:11.000000000 -0400 ++++ /tmp/cvc4_stdout.D4XU59TzLS 2010-07-10 18:02:11.000000000 -0400 +@@ -1 +0,0 @@ +-UNSAT +run_regression: error: differences between expected and actual output on stderr +--- /tmp/cvc4_expect_stderr.wOxDVDJHO2 2010-07-10 18:02:11.000000000 -0400 ++++ /tmp/cvc4_stderr.3GR7s0o4Qj 2010-07-10 18:02:11.000000000 -0400 +@@ -0,0 +1,2 @@ ++CVC4 suffered a segfault. ++/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/uf/../../run_regression: line 137: 2293 Aborted "$cvc4full" --segv-nospin `basename "$benchmark"` +run_regression: error: expected exit status `20' but got `134' + +FAIL: iso_brn001.smt (exit: 1) +============================== + +running /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/main/cvc4 iso_brn001.smt from /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/uf +run_regression: error: differences between expected and actual output on stdout +--- /tmp/cvc4_expect_stdout.XdVfpRvCZi 2010-07-10 18:02:11.000000000 -0400 ++++ /tmp/cvc4_stdout.TVSlnfo7Fz 2010-07-10 18:02:11.000000000 -0400 +@@ -1 +0,0 @@ +-SAT +run_regression: error: differences between expected and actual output on stderr +--- /tmp/cvc4_expect_stderr.dAimWgRvdF 2010-07-10 18:02:11.000000000 -0400 ++++ /tmp/cvc4_stderr.bZCfoGJXrR 2010-07-10 18:02:11.000000000 -0400 +@@ -0,0 +1,2 @@ ++CVC4 suffered a segfault. ++/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/uf/../../run_regression: line 137: 2374 Aborted "$cvc4full" --segv-nospin `basename "$benchmark"` +run_regression: error: expected exit status `10' but got `134' + +FAIL: SEQ032_size2.smt (exit: 1) +================================ + +running /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/main/cvc4 SEQ032_size2.smt from /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/uf +run_regression: error: differences between expected and actual output on stdout +--- /tmp/cvc4_expect_stdout.E6LpmzK4g0 2010-07-10 18:02:12.000000000 -0400 ++++ /tmp/cvc4_stdout.5yKM5G4IrU 2010-07-10 18:02:12.000000000 -0400 +@@ -1 +0,0 @@ +-UNSAT +run_regression: error: differences between expected and actual output on stderr +--- /tmp/cvc4_expect_stderr.iQjfnFBT7X 2010-07-10 18:02:12.000000000 -0400 ++++ /tmp/cvc4_stderr.gEPJOwJQRi 2010-07-10 18:02:12.000000000 -0400 +@@ -0,0 +1,2 @@ ++CVC4 suffered a segfault. ++/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/uf/../../run_regression: line 137: 2415 Aborted "$cvc4full" --segv-nospin `basename "$benchmark"` +run_regression: error: expected exit status `20' but got `134' + +FAIL: simple.01.cvc (exit: 1) +============================= + +running /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/main/cvc4 simple.01.cvc from /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/uf +run_regression: error: differences between expected and actual output on stdout +--- /tmp/cvc4_expect_stdout.gQgfJOYqO0 2010-07-10 18:02:12.000000000 -0400 ++++ /tmp/cvc4_stdout.j2txKjzlWw 2010-07-10 18:02:12.000000000 -0400 +@@ -1 +0,0 @@ +-VALID +run_regression: error: differences between expected and actual output on stderr +--- /tmp/cvc4_expect_stderr.OmrcHiE0bm 2010-07-10 18:02:12.000000000 -0400 ++++ /tmp/cvc4_stderr.ApWWj8TODo 2010-07-10 18:02:12.000000000 -0400 +@@ -0,0 +1,2 @@ ++CVC4 suffered a segfault. ++/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/uf/../../run_regression: line 137: 2464 Aborted "$cvc4full" --segv-nospin `basename "$benchmark"` +run_regression: error: expected exit status `20' but got `134' + +FAIL: simple.02.cvc (exit: 1) +============================= + +running /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/main/cvc4 simple.02.cvc from /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/uf +run_regression: error: differences between expected and actual output on stdout +--- /tmp/cvc4_expect_stdout.zfLiVzdNq3 2010-07-10 18:02:12.000000000 -0400 ++++ /tmp/cvc4_stdout.G8Z2Fa4ubE 2010-07-10 18:02:12.000000000 -0400 +@@ -1 +0,0 @@ +-INVALID +run_regression: error: differences between expected and actual output on stderr +--- /tmp/cvc4_expect_stderr.czVSjhEPMf 2010-07-10 18:02:12.000000000 -0400 ++++ /tmp/cvc4_stderr.FO82xPjjPy 2010-07-10 18:02:12.000000000 -0400 +@@ -0,0 +1,2 @@ ++CVC4 suffered a segfault. ++/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/uf/../../run_regression: line 137: 2513 Aborted "$cvc4full" --segv-nospin `basename "$benchmark"` +run_regression: error: expected exit status `10' but got `134' + +FAIL: simple.03.cvc (exit: 1) +============================= + +running /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/main/cvc4 simple.03.cvc from /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/uf +run_regression: error: differences between expected and actual output on stdout +--- /tmp/cvc4_expect_stdout.3ST08Nkz9u 2010-07-10 18:02:12.000000000 -0400 ++++ /tmp/cvc4_stdout.uPIc1aoM2T 2010-07-10 18:02:12.000000000 -0400 +@@ -1 +0,0 @@ +-VALID +run_regression: error: differences between expected and actual output on stderr +--- /tmp/cvc4_expect_stderr.RKx6HgIFuX 2010-07-10 18:02:12.000000000 -0400 ++++ /tmp/cvc4_stderr.KXtNgL89ua 2010-07-10 18:02:12.000000000 -0400 +@@ -0,0 +1,2 @@ ++CVC4 suffered a segfault. ++/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/uf/../../run_regression: line 137: 2563 Aborted "$cvc4full" --segv-nospin `basename "$benchmark"` +run_regression: error: expected exit status `20' but got `134' + +FAIL: simple.04.cvc (exit: 1) +============================= + +running /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/src/main/cvc4 simple.04.cvc from /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/uf +run_regression: error: differences between expected and actual output on stdout +--- /tmp/cvc4_expect_stdout.HNSKjr84Tw 2010-07-10 18:02:12.000000000 -0400 ++++ /tmp/cvc4_stdout.imKc1ONSt9 2010-07-10 18:02:12.000000000 -0400 +@@ -1 +0,0 @@ +-INVALID +run_regression: error: differences between expected and actual output on stderr +--- /tmp/cvc4_expect_stderr.Ld90a7Tz4k 2010-07-10 18:02:12.000000000 -0400 ++++ /tmp/cvc4_stderr.jdNJ4Y2UvI 2010-07-10 18:02:12.000000000 -0400 +@@ -0,0 +1,2 @@ ++CVC4 suffered a segfault. ++/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/../../../test/regress/regress0/uf/../../run_regression: line 137: 2612 Aborted "$cvc4full" --segv-nospin `basename "$benchmark"` +run_regression: error: expected exit status `10' but got `134' +=========================================== +18 of 19 tests failed +See test/regress/regress0/uf/test-suite.log +=========================================== +make[8]: *** [test-suite.log] Error 1 +make[8]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/regress/regress0/uf' +make[7]: *** [check-TESTS] Error 2 +make[7]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/regress/regress0/uf' +make[6]: *** [check-am] Error 2 +make[6]: Target `check' not remade because of errors. +make[6]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/regress/regress0/uf' +make[5]: *** [check-recursive] Error 1 +make[5]: Target `check' not remade because of errors. +make[5]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/regress/regress0' +make[5]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/regress' +make[5]: Nothing to be done for `check-am'. +make[5]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/regress' +make[4]: *** [check-recursive] Error 1 +make[4]: Target `check' not remade because of errors. +make[4]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/regress' +Making check in . +make[4]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test' +make check-local +make[5]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test' +=============================== TESTING SUMMARY ============================= +1 of 35 tests failed. + /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/unit/test-suite.log +All 0 tests passed. in system +7 of 65 tests failed. + /home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test/regress/regress0/test-suite.log +=============================== TESTING SUMMARY ============================= +make[5]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test' +make[4]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test' +make[3]: *** [check-recursive] Error 1 +make[3]: Target `check' not remade because of errors. +make[3]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/test' +Making check in contrib +make[3]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/contrib' +make[3]: Nothing to be done for `check'. +make[3]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition/contrib' +make[3]: Entering directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition' +make[3]: Nothing to be done for `check-am'. +make[3]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition' +make[2]: *** [check-recursive] Error 1 +make[2]: Target `check' not remade because of errors. +make[2]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds/x86_64-unknown-linux-gnu/competition' +make[1]: *** [check] Error 2 +make[1]: Leaving directory `/home/mdeters/cvc4-smtcomp2010/builds' +make: *** [check] Error 2 ++ true ++ mkdir cvc4-1.0a0-smtcomp2010 ++ cp smtcomp2010-runscript cvc4-1.0a0-smtcomp2010/run ++ chmod 755 cvc4-1.0a0-smtcomp2010/run ++ cp builds/bin/cvc4 cvc4-1.0a0-smtcomp2010/cvc4 ++ tar cfzv cvc4-1.0a0-smtcomp2010.tgz cvc4-1.0a0-smtcomp2010 +cvc4-1.0a0-smtcomp2010/ +cvc4-1.0a0-smtcomp2010/run +cvc4-1.0a0-smtcomp2010/cvc4 |