Attachment 420261 Details for Bug 599887 – build.log

build.log

build.log (text/plain), 71.31 KB, created by FTBFS on 2010-06-03 20:46:17 UTC

(hide)

Description:

Filename:

MIME Type:

Creator: FTBFS

Created: 2010-06-03 20:46:17 UTC

Size: 71.31 KB

patch

obsolete

>Mock Version: 1.1.1
>ENTER do(['bash', '--login', '-c', 'rpmbuild -bs --target x86_64 --nodeps builddir/build/SPECS/cvc3.spec'], False, '/var/lib/mock/fedora-development-x86_64-cvc3-2.2-1.fc13.src.rpm/root/', None, 25200, True, 0, 8116, 14667, None, logger=<mock.trace_decorator.getLog object at 0x1771b90>)
>Executing command: ['bash', '--login', '-c', 'rpmbuild -bs --target x86_64 --nodeps builddir/build/SPECS/cvc3.spec']
>Building target platforms: x86_64
>Building for target x86_64
>Wrote: /builddir/build/SRPMS/cvc3-2.2-1.fc14.src.rpm
>Child returncode was: 0
>LEAVE do --> 
>
>ENTER do(['bash', '--login', '-c', 'rpmbuild -bb --target x86_64 --nodeps builddir/build/SPECS/cvc3.spec'], False, '/var/lib/mock/fedora-development-x86_64-cvc3-2.2-1.fc13.src.rpm/root/', None, 25200, True, 0, 8116, 14667, None, logger=<mock.trace_decorator.getLog object at 0x1771b90>)
>Executing command: ['bash', '--login', '-c', 'rpmbuild -bb --target x86_64 --nodeps builddir/build/SPECS/cvc3.spec']
>Building target platforms: x86_64
>Building for target x86_64
>Executing(%prep): /bin/sh -e /var/tmp/rpm-tmp.L32mbE
>+ umask 022
>+ cd /builddir/build/BUILD
>+ LANG=C
>+ export LANG
>+ unset DISPLAY
>+ cd /builddir/build/BUILD
>+ rm -rf cvc3-2.2
>+ /usr/bin/gzip -dc /builddir/build/SOURCES/cvc3-2.2.tar.gz
>+ /bin/tar -xf -
>+ STATUS=0
>+ '[' 0 -ne 0 ']'
>+ cd cvc3-2.2
>+ /bin/chmod -Rf a+rX,u+w,g-w,o-w .
>Patch #0 (cvc3-build.patch):
>+ echo 'Patch #0 (cvc3-build.patch):'
>+ /bin/cat /builddir/build/SOURCES/cvc3-build.patch
>+ /usr/bin/patch -s -p1 --fuzz=0
>Patch #1 (cvc3-doc.patch):
>+ echo 'Patch #1 (cvc3-doc.patch):'
>+ /bin/cat /builddir/build/SOURCES/cvc3-doc.patch
>+ /usr/bin/patch -s -p1 --fuzz=0
>+ sed -i -e 's|loadLibrary("cvc3jni")|load("/usr/lib64/cvc3/libcvc3jni.so")|' java/src/cvc3/Embedded.java
>+ exit 0
>Executing(%build): /bin/sh -e /var/tmp/rpm-tmp.jvwh9m
>+ umask 022
>+ cd /builddir/build/BUILD
>+ cd cvc3-2.2
>+ LANG=C
>+ export LANG
>+ unset DISPLAY
>+ CFLAGS='-O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic'
>+ export CFLAGS
>+ CXXFLAGS='-O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic'
>+ export CXXFLAGS
>+ FFLAGS='-O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -I/usr/lib64/gfortran/modules'
>+ export FFLAGS
>+ ./configure --build=x86_64-unknown-linux-gnu --host=x86_64-unknown-linux-gnu --program-prefix= --disable-dependency-tracking --prefix=/usr --exec-prefix=/usr --bindir=/usr/bin --sbindir=/usr/sbin --sysconfdir=/etc --datadir=/usr/share --includedir=/usr/include --libdir=/usr/lib64 --libexecdir=/usr/libexec --localstatedir=/var --sharedstatedir=/var/lib --mandir=/usr/share/man --infodir=/usr/share/info --with-build=optimized --enable-dynamic --enable-java --with-java-home=/usr/lib/jvm/java
>checking for x86_64-unknown-linux-gnu-g++... no
>checking for x86_64-unknown-linux-gnu-c++... no
>checking for x86_64-unknown-linux-gnu-gpp... no
>checking for x86_64-unknown-linux-gnu-aCC... no
>checking for x86_64-unknown-linux-gnu-CC... no
>checking for x86_64-unknown-linux-gnu-cxx... no
>checking for x86_64-unknown-linux-gnu-cc++... no
>checking for x86_64-unknown-linux-gnu-cl... no
>checking for x86_64-unknown-linux-gnu-FCC... no
>checking for x86_64-unknown-linux-gnu-KCC... no
>checking for x86_64-unknown-linux-gnu-RCC... no
>checking for x86_64-unknown-linux-gnu-xlC_r... no
>checking for x86_64-unknown-linux-gnu-xlC... no
>checking for g++... g++
>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 g++ accepts -g... yes
>checking how to run the C++ preprocessor... g++ -E
>checking for x86_64-unknown-linux-gnu-ar... no
>checking for ar... ar
>checking build system type... x86_64-unknown-linux-gnu
>checking host system type... x86_64-unknown-linux-gnu
>checking for install... /usr/bin/install
>checking for time... /usr/bin/time
>checking for perl... /usr/bin/perl
>checking for bison... bison -y
>checking for flex... flex
>checking for yywrap in -lfl... yes
>checking lex output file root... lex.yy
>checking whether yytext is a pointer... no
>checking for compiler version (g++ --version)... 4.4.4
>checking for gmp... yes
>checking for javac... /usr/lib/jvm/java/bin/javac
>checking for javah... /usr/lib/jvm/java/bin/javah
>checking for jar... /usr/lib/jvm/java/bin/jar
>checking for java... /usr/lib/jvm/java/bin/java
>checking for egrep... grep -E
>checking for ANSI C header files... yes
>checking for sys/types.h... yes
>checking for sys/stat.h... yes
>checking for stdlib.h... yes
>checking for string.h... yes
>checking for memory.h... yes
>checking for strings.h... yes
>checking for inttypes.h... yes
>checking for stdint.h... yes
>checking for unistd.h... yes
>checking jni.h usability... yes
>checking jni.h presence... yes
>checking for jni.h... yes
>checking jni_md.h usability... yes
>checking jni_md.h presence... yes
>checking for jni_md.h... yes
>checking for python... ./configure: line 4380: error:: command not found
>no
>checking vector usability... yes
>checking vector presence... yes
>checking for vector... yes
>checking list usability... yes
>checking list presence... yes
>checking for list... yes
>checking deque usability... yes
>checking deque presence... yes
>checking for deque... yes
>checking set usability... yes
>checking set presence... yes
>checking for set... yes
>checking string usability... yes
>checking string presence... yes
>checking for string... yes
>checking cstdlib usability... yes
>checking cstdlib presence... yes
>checking for cstdlib... yes
>checking cstdio usability... yes
>checking cstdio presence... yes
>checking for cstdio... yes
>checking functional usability... yes
>checking functional presence... yes
>checking for functional... yes
>checking algorithm usability... yes
>checking algorithm presence... yes
>checking for algorithm... yes
>checking for doxygen... doxygen
>checking for doxytag... doxytag
>checking for fig2dev... fig2dev
>checking for dot... NO
>checking for etags... etags
>checking for ebrowse... ebrowse
>configure: creating ./config.status
>config.status: creating Makefile.local
>config.status: creating LICENSE
>config.status: creating bin/unpack
>config.status: creating bin/run_tests
>config.status: creating bin/cvc2smt
>config.status: creating doc/Doxyfile
>config.status: creating doc/Makefile
>CVC3 is configured successfully.
>Platform: x86_64-linux-gnu
>Version: 2.2
>Computer arithmetic: GMP
>Run ./configure --help for additional configuration options.
>Type 'make' to compile CVC3.
>*** CVC3 is configured to compile using shared libraries.
>*** Type "make ld_sh" for bash shells or "make ld_csh" for csh shells
>*** to see how to set LD_LIBRARY_PATH appropriately.  To use static
>*** libraries and executables instead, run:
>***     ./configure --enable-static
>+ make -j8
>cd /builddir/build/BUILD/cvc3-2.2/src; make  VERSION=2.2
>make[1]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src'
>cd util && make 
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/util'
>Making dependencies for debug.cpp statistics.cpp rational.cpp rational-native.cpp rational-gmp.cpp
>g++ -M -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include -DRATIONAL_GMP  debug.cpp statistics.cpp rational.cpp rational-native.cpp rational-gmp.cpp >> /builddir/build/BUILD/cvc3-2.2/obj/util/x86_64-linux-gnu/Makefile.tmp
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/util'
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/util'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include -DRATIONAL_GMP  -c debug.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/util/x86_64-linux-gnu/debug.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include -DRATIONAL_GMP  -c statistics.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/util/x86_64-linux-gnu/statistics.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include -DRATIONAL_GMP  -c rational.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/util/x86_64-linux-gnu/rational.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include -DRATIONAL_GMP  -c rational-native.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/util/x86_64-linux-gnu/rational-native.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include -DRATIONAL_GMP  -c rational-gmp.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/util/x86_64-linux-gnu/rational-gmp.o'
>ar ruvs '/builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libcvc_util.a'  /builddir/build/BUILD/cvc3-2.2/obj/util/x86_64-linux-gnu/debug.o  /builddir/build/BUILD/cvc3-2.2/obj/util/x86_64-linux-gnu/statistics.o  /builddir/build/BUILD/cvc3-2.2/obj/util/x86_64-linux-gnu/rational.o  /builddir/build/BUILD/cvc3-2.2/obj/util/x86_64-linux-gnu/rational-native.o  /builddir/build/BUILD/cvc3-2.2/obj/util/x86_64-linux-gnu/rational-gmp.o 
>ar: creating /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libcvc_util.a
>a - /builddir/build/BUILD/cvc3-2.2/obj/util/x86_64-linux-gnu/debug.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/util/x86_64-linux-gnu/statistics.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/util/x86_64-linux-gnu/rational.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/util/x86_64-linux-gnu/rational-native.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/util/x86_64-linux-gnu/rational-gmp.o
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/util'
>cd context && make 
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/context'
>Making dependencies for context.cpp cdflags.cpp
>g++ -M -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  context.cpp cdflags.cpp >> /builddir/build/BUILD/cvc3-2.2/obj/context/x86_64-linux-gnu/Makefile.tmp
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/context'
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/context'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c context.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/context/x86_64-linux-gnu/context.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c cdflags.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/context/x86_64-linux-gnu/cdflags.o'
>ar ruvs '/builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libcontext.a'  /builddir/build/BUILD/cvc3-2.2/obj/context/x86_64-linux-gnu/context.o  /builddir/build/BUILD/cvc3-2.2/obj/context/x86_64-linux-gnu/cdflags.o 
>ar: creating /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libcontext.a
>a - /builddir/build/BUILD/cvc3-2.2/obj/context/x86_64-linux-gnu/context.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/context/x86_64-linux-gnu/cdflags.o
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/context'
>cd expr && make 
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/expr'
>Making dependencies for expr.cpp expr_manager.cpp expr_stream.cpp expr_value.cpp expr_op.cpp
>g++ -M -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  expr.cpp expr_manager.cpp expr_stream.cpp expr_value.cpp expr_op.cpp >> /builddir/build/BUILD/cvc3-2.2/obj/expr/x86_64-linux-gnu/Makefile.tmp
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/expr'
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/expr'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c expr.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/expr/x86_64-linux-gnu/expr.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c expr_manager.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/expr/x86_64-linux-gnu/expr_manager.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c expr_stream.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/expr/x86_64-linux-gnu/expr_stream.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c expr_value.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/expr/x86_64-linux-gnu/expr_value.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c expr_op.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/expr/x86_64-linux-gnu/expr_op.o'
>ar ruvs '/builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libexpr.a'  /builddir/build/BUILD/cvc3-2.2/obj/expr/x86_64-linux-gnu/expr.o  /builddir/build/BUILD/cvc3-2.2/obj/expr/x86_64-linux-gnu/expr_manager.o  /builddir/build/BUILD/cvc3-2.2/obj/expr/x86_64-linux-gnu/expr_stream.o  /builddir/build/BUILD/cvc3-2.2/obj/expr/x86_64-linux-gnu/expr_value.o  /builddir/build/BUILD/cvc3-2.2/obj/expr/x86_64-linux-gnu/expr_op.o 
>ar: creating /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libexpr.a
>a - /builddir/build/BUILD/cvc3-2.2/obj/expr/x86_64-linux-gnu/expr.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/expr/x86_64-linux-gnu/expr_manager.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/expr/x86_64-linux-gnu/expr_stream.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/expr/x86_64-linux-gnu/expr_value.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/expr/x86_64-linux-gnu/expr_op.o
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/expr'
>cd theorem && make 
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/theorem'
>Making dependencies for assumptions.cpp theorem.cpp theorem_manager.cpp theorem_producer.cpp common_theorem_producer.cpp
>g++ -M -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  assumptions.cpp theorem.cpp theorem_manager.cpp theorem_producer.cpp common_theorem_producer.cpp >> /builddir/build/BUILD/cvc3-2.2/obj/theorem/x86_64-linux-gnu/Makefile.tmp
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/theorem'
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/theorem'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c assumptions.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/theorem/x86_64-linux-gnu/assumptions.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c theorem.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/theorem/x86_64-linux-gnu/theorem.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c theorem_manager.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/theorem/x86_64-linux-gnu/theorem_manager.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c theorem_producer.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/theorem/x86_64-linux-gnu/theorem_producer.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c common_theorem_producer.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/theorem/x86_64-linux-gnu/common_theorem_producer.o'
>ar ruvs '/builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libtheorem.a'  /builddir/build/BUILD/cvc3-2.2/obj/theorem/x86_64-linux-gnu/assumptions.o  /builddir/build/BUILD/cvc3-2.2/obj/theorem/x86_64-linux-gnu/theorem.o  /builddir/build/BUILD/cvc3-2.2/obj/theorem/x86_64-linux-gnu/theorem_manager.o  /builddir/build/BUILD/cvc3-2.2/obj/theorem/x86_64-linux-gnu/theorem_producer.o  /builddir/build/BUILD/cvc3-2.2/obj/theorem/x86_64-linux-gnu/common_theorem_producer.o 
>ar: creating /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libtheorem.a
>a - /builddir/build/BUILD/cvc3-2.2/obj/theorem/x86_64-linux-gnu/assumptions.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/theorem/x86_64-linux-gnu/theorem.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/theorem/x86_64-linux-gnu/theorem_manager.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/theorem/x86_64-linux-gnu/theorem_producer.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/theorem/x86_64-linux-gnu/common_theorem_producer.o
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/theorem'
>cd sat && make 
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/sat'
>Making dependencies for  cnf.cpp cnf_manager.cpp cnf_theorem_producer.cpp dpllt_basic.cpp sat_api.cpp dpllt_minisat.cpp minisat_types.cpp minisat_derivation.cpp minisat_solver.cpp
>g++ -M -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include    cnf.cpp cnf_manager.cpp cnf_theorem_producer.cpp dpllt_basic.cpp sat_api.cpp dpllt_minisat.cpp minisat_types.cpp minisat_derivation.cpp minisat_solver.cpp >> /builddir/build/BUILD/cvc3-2.2/obj/sat/x86_64-linux-gnu/Makefile.tmp
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/sat'
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/sat'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include   -c cnf_manager.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/sat/x86_64-linux-gnu/cnf_manager.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include   -c cnf.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/sat/x86_64-linux-gnu/cnf.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include   -c cnf_theorem_producer.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/sat/x86_64-linux-gnu/cnf_theorem_producer.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include   -c dpllt_basic.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/sat/x86_64-linux-gnu/dpllt_basic.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include   -c sat_api.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/sat/x86_64-linux-gnu/sat_api.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include   -c dpllt_minisat.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/sat/x86_64-linux-gnu/dpllt_minisat.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include   -c minisat_types.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/sat/x86_64-linux-gnu/minisat_types.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include   -c minisat_derivation.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/sat/x86_64-linux-gnu/minisat_derivation.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include   -c minisat_solver.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/sat/x86_64-linux-gnu/minisat_solver.o'
>ar ruvs '/builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libsat.a'  /builddir/build/BUILD/cvc3-2.2/obj/sat/x86_64-linux-gnu/cnf.o  /builddir/build/BUILD/cvc3-2.2/obj/sat/x86_64-linux-gnu/cnf_manager.o  /builddir/build/BUILD/cvc3-2.2/obj/sat/x86_64-linux-gnu/cnf_theorem_producer.o  /builddir/build/BUILD/cvc3-2.2/obj/sat/x86_64-linux-gnu/dpllt_basic.o  /builddir/build/BUILD/cvc3-2.2/obj/sat/x86_64-linux-gnu/sat_api.o  /builddir/build/BUILD/cvc3-2.2/obj/sat/x86_64-linux-gnu/dpllt_minisat.o  /builddir/build/BUILD/cvc3-2.2/obj/sat/x86_64-linux-gnu/minisat_types.o  /builddir/build/BUILD/cvc3-2.2/obj/sat/x86_64-linux-gnu/minisat_derivation.o  /builddir/build/BUILD/cvc3-2.2/obj/sat/x86_64-linux-gnu/minisat_solver.o 
>ar: creating /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libsat.a
>a - /builddir/build/BUILD/cvc3-2.2/obj/sat/x86_64-linux-gnu/cnf.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/sat/x86_64-linux-gnu/cnf_manager.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/sat/x86_64-linux-gnu/cnf_theorem_producer.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/sat/x86_64-linux-gnu/dpllt_basic.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/sat/x86_64-linux-gnu/sat_api.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/sat/x86_64-linux-gnu/dpllt_minisat.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/sat/x86_64-linux-gnu/minisat_types.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/sat/x86_64-linux-gnu/minisat_derivation.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/sat/x86_64-linux-gnu/minisat_solver.o
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/sat'
>cd theory_core && make 
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/theory_core'
>Making dependencies for theory.cpp theory_core.cpp core_theorem_producer.cpp expr_transform.cpp bryant.cpp
>g++ -M -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  theory.cpp theory_core.cpp core_theorem_producer.cpp expr_transform.cpp bryant.cpp >> /builddir/build/BUILD/cvc3-2.2/obj/theory_core/x86_64-linux-gnu/Makefile.tmp
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/theory_core'
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/theory_core'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c theory.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/theory_core/x86_64-linux-gnu/theory.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c theory_core.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/theory_core/x86_64-linux-gnu/theory_core.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c core_theorem_producer.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/theory_core/x86_64-linux-gnu/core_theorem_producer.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c expr_transform.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/theory_core/x86_64-linux-gnu/expr_transform.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c bryant.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/theory_core/x86_64-linux-gnu/bryant.o'
>ar ruvs '/builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libtheory_core.a'  /builddir/build/BUILD/cvc3-2.2/obj/theory_core/x86_64-linux-gnu/theory.o  /builddir/build/BUILD/cvc3-2.2/obj/theory_core/x86_64-linux-gnu/theory_core.o  /builddir/build/BUILD/cvc3-2.2/obj/theory_core/x86_64-linux-gnu/core_theorem_producer.o  /builddir/build/BUILD/cvc3-2.2/obj/theory_core/x86_64-linux-gnu/expr_transform.o  /builddir/build/BUILD/cvc3-2.2/obj/theory_core/x86_64-linux-gnu/bryant.o 
>ar: creating /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libtheory_core.a
>a - /builddir/build/BUILD/cvc3-2.2/obj/theory_core/x86_64-linux-gnu/theory.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/theory_core/x86_64-linux-gnu/theory_core.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/theory_core/x86_64-linux-gnu/core_theorem_producer.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/theory_core/x86_64-linux-gnu/expr_transform.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/theory_core/x86_64-linux-gnu/bryant.o
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/theory_core'
>cd theory_arith && make 
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/theory_arith'
>Making dependencies for arith_theorem_producer_old.cpp arith_theorem_producer.cpp arith_theorem_producer3.cpp theory_arith.cpp theory_arith_old.cpp theory_arith_new.cpp theory_arith3.cpp
>g++ -M -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  arith_theorem_producer_old.cpp arith_theorem_producer.cpp arith_theorem_producer3.cpp theory_arith.cpp theory_arith_old.cpp theory_arith_new.cpp theory_arith3.cpp >> /builddir/build/BUILD/cvc3-2.2/obj/theory_arith/x86_64-linux-gnu/Makefile.tmp
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/theory_arith'
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/theory_arith'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c arith_theorem_producer_old.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer_old.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c arith_theorem_producer.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c arith_theorem_producer3.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer3.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c theory_arith.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/theory_arith/x86_64-linux-gnu/theory_arith.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c theory_arith_old.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/theory_arith/x86_64-linux-gnu/theory_arith_old.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c theory_arith_new.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/theory_arith/x86_64-linux-gnu/theory_arith_new.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c theory_arith3.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/theory_arith/x86_64-linux-gnu/theory_arith3.o'
>ar ruvs '/builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libtheory_arith.a'  /builddir/build/BUILD/cvc3-2.2/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer_old.o  /builddir/build/BUILD/cvc3-2.2/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer.o  /builddir/build/BUILD/cvc3-2.2/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer3.o  /builddir/build/BUILD/cvc3-2.2/obj/theory_arith/x86_64-linux-gnu/theory_arith.o  /builddir/build/BUILD/cvc3-2.2/obj/theory_arith/x86_64-linux-gnu/theory_arith_old.o  /builddir/build/BUILD/cvc3-2.2/obj/theory_arith/x86_64-linux-gnu/theory_arith_new.o  /builddir/build/BUILD/cvc3-2.2/obj/theory_arith/x86_64-linux-gnu/theory_arith3.o 
>ar: creating /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libtheory_arith.a
>a - /builddir/build/BUILD/cvc3-2.2/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer_old.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer3.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/theory_arith/x86_64-linux-gnu/theory_arith.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/theory_arith/x86_64-linux-gnu/theory_arith_old.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/theory_arith/x86_64-linux-gnu/theory_arith_new.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/theory_arith/x86_64-linux-gnu/theory_arith3.o
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/theory_arith'
>cd theory_array && make 
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/theory_array'
>Making dependencies for array_theorem_producer.cpp theory_array.cpp
>g++ -M -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  array_theorem_producer.cpp theory_array.cpp >> /builddir/build/BUILD/cvc3-2.2/obj/theory_array/x86_64-linux-gnu/Makefile.tmp
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/theory_array'
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/theory_array'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c array_theorem_producer.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/theory_array/x86_64-linux-gnu/array_theorem_producer.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c theory_array.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/theory_array/x86_64-linux-gnu/theory_array.o'
>ar ruvs '/builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libtheory_array.a'  /builddir/build/BUILD/cvc3-2.2/obj/theory_array/x86_64-linux-gnu/array_theorem_producer.o  /builddir/build/BUILD/cvc3-2.2/obj/theory_array/x86_64-linux-gnu/theory_array.o 
>ar: creating /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libtheory_array.a
>a - /builddir/build/BUILD/cvc3-2.2/obj/theory_array/x86_64-linux-gnu/array_theorem_producer.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/theory_array/x86_64-linux-gnu/theory_array.o
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/theory_array'
>cd theory_bitvector && make 
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/theory_bitvector'
>Making dependencies for bitvector_theorem_producer.cpp theory_bitvector.cpp
>g++ -M -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  bitvector_theorem_producer.cpp theory_bitvector.cpp >> /builddir/build/BUILD/cvc3-2.2/obj/theory_bitvector/x86_64-linux-gnu/Makefile.tmp
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/theory_bitvector'
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/theory_bitvector'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c bitvector_theorem_producer.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/theory_bitvector/x86_64-linux-gnu/bitvector_theorem_producer.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c theory_bitvector.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/theory_bitvector/x86_64-linux-gnu/theory_bitvector.o'
>ar ruvs '/builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libtheory_bitvector.a'  /builddir/build/BUILD/cvc3-2.2/obj/theory_bitvector/x86_64-linux-gnu/bitvector_theorem_producer.o  /builddir/build/BUILD/cvc3-2.2/obj/theory_bitvector/x86_64-linux-gnu/theory_bitvector.o 
>ar: creating /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libtheory_bitvector.a
>a - /builddir/build/BUILD/cvc3-2.2/obj/theory_bitvector/x86_64-linux-gnu/bitvector_theorem_producer.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/theory_bitvector/x86_64-linux-gnu/theory_bitvector.o
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/theory_bitvector'
>cd theory_datatype && make 
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/theory_datatype'
>Making dependencies for datatype_theorem_producer.cpp theory_datatype.cpp theory_datatype_lazy.cpp
>g++ -M -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  datatype_theorem_producer.cpp theory_datatype.cpp theory_datatype_lazy.cpp >> /builddir/build/BUILD/cvc3-2.2/obj/theory_datatype/x86_64-linux-gnu/Makefile.tmp
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/theory_datatype'
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/theory_datatype'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c datatype_theorem_producer.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/theory_datatype/x86_64-linux-gnu/datatype_theorem_producer.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c theory_datatype.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/theory_datatype/x86_64-linux-gnu/theory_datatype.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c theory_datatype_lazy.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/theory_datatype/x86_64-linux-gnu/theory_datatype_lazy.o'
>ar ruvs '/builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libtheory_datatype.a'  /builddir/build/BUILD/cvc3-2.2/obj/theory_datatype/x86_64-linux-gnu/datatype_theorem_producer.o  /builddir/build/BUILD/cvc3-2.2/obj/theory_datatype/x86_64-linux-gnu/theory_datatype.o  /builddir/build/BUILD/cvc3-2.2/obj/theory_datatype/x86_64-linux-gnu/theory_datatype_lazy.o 
>ar: creating /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libtheory_datatype.a
>a - /builddir/build/BUILD/cvc3-2.2/obj/theory_datatype/x86_64-linux-gnu/datatype_theorem_producer.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/theory_datatype/x86_64-linux-gnu/theory_datatype.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/theory_datatype/x86_64-linux-gnu/theory_datatype_lazy.o
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/theory_datatype'
>cd theory_quant && make 
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/theory_quant'
>Making dependencies for theory_quant.cpp quant_theorem_producer.cpp
>g++ -M -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  theory_quant.cpp quant_theorem_producer.cpp >> /builddir/build/BUILD/cvc3-2.2/obj/theory_quant/x86_64-linux-gnu/Makefile.tmp
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/theory_quant'
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/theory_quant'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c theory_quant.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/theory_quant/x86_64-linux-gnu/theory_quant.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c quant_theorem_producer.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/theory_quant/x86_64-linux-gnu/quant_theorem_producer.o'
>ar ruvs '/builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libtheory_quant.a'  /builddir/build/BUILD/cvc3-2.2/obj/theory_quant/x86_64-linux-gnu/theory_quant.o  /builddir/build/BUILD/cvc3-2.2/obj/theory_quant/x86_64-linux-gnu/quant_theorem_producer.o 
>ar: creating /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libtheory_quant.a
>a - /builddir/build/BUILD/cvc3-2.2/obj/theory_quant/x86_64-linux-gnu/theory_quant.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/theory_quant/x86_64-linux-gnu/quant_theorem_producer.o
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/theory_quant'
>cd theory_records && make 
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/theory_records'
>Making dependencies for theory_records.cpp records_theorem_producer.cpp
>g++ -M -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  theory_records.cpp records_theorem_producer.cpp >> /builddir/build/BUILD/cvc3-2.2/obj/theory_records/x86_64-linux-gnu/Makefile.tmp
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/theory_records'
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/theory_records'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c theory_records.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/theory_records/x86_64-linux-gnu/theory_records.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c records_theorem_producer.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/theory_records/x86_64-linux-gnu/records_theorem_producer.o'
>ar ruvs '/builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libtheory_records.a'  /builddir/build/BUILD/cvc3-2.2/obj/theory_records/x86_64-linux-gnu/theory_records.o  /builddir/build/BUILD/cvc3-2.2/obj/theory_records/x86_64-linux-gnu/records_theorem_producer.o 
>ar: creating /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libtheory_records.a
>a - /builddir/build/BUILD/cvc3-2.2/obj/theory_records/x86_64-linux-gnu/theory_records.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/theory_records/x86_64-linux-gnu/records_theorem_producer.o
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/theory_records'
>cd theory_simulate && make 
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/theory_simulate'
>Making dependencies for theory_simulate.cpp simulate_theorem_producer.cpp
>g++ -M -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  theory_simulate.cpp simulate_theorem_producer.cpp >> /builddir/build/BUILD/cvc3-2.2/obj/theory_simulate/x86_64-linux-gnu/Makefile.tmp
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/theory_simulate'
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/theory_simulate'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c theory_simulate.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/theory_simulate/x86_64-linux-gnu/theory_simulate.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c simulate_theorem_producer.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/theory_simulate/x86_64-linux-gnu/simulate_theorem_producer.o'
>ar ruvs '/builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libtheory_simulate.a'  /builddir/build/BUILD/cvc3-2.2/obj/theory_simulate/x86_64-linux-gnu/theory_simulate.o  /builddir/build/BUILD/cvc3-2.2/obj/theory_simulate/x86_64-linux-gnu/simulate_theorem_producer.o 
>ar: creating /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libtheory_simulate.a
>a - /builddir/build/BUILD/cvc3-2.2/obj/theory_simulate/x86_64-linux-gnu/theory_simulate.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/theory_simulate/x86_64-linux-gnu/simulate_theorem_producer.o
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/theory_simulate'
>cd theory_uf && make 
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/theory_uf'
>Making dependencies for uf_theorem_producer.cpp theory_uf.cpp
>g++ -M -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  uf_theorem_producer.cpp theory_uf.cpp >> /builddir/build/BUILD/cvc3-2.2/obj/theory_uf/x86_64-linux-gnu/Makefile.tmp
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/theory_uf'
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/theory_uf'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c uf_theorem_producer.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/theory_uf/x86_64-linux-gnu/uf_theorem_producer.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c theory_uf.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/theory_uf/x86_64-linux-gnu/theory_uf.o'
>ar ruvs '/builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libtheory_uf.a'  /builddir/build/BUILD/cvc3-2.2/obj/theory_uf/x86_64-linux-gnu/uf_theorem_producer.o  /builddir/build/BUILD/cvc3-2.2/obj/theory_uf/x86_64-linux-gnu/theory_uf.o 
>ar: creating /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libtheory_uf.a
>a - /builddir/build/BUILD/cvc3-2.2/obj/theory_uf/x86_64-linux-gnu/uf_theorem_producer.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/theory_uf/x86_64-linux-gnu/theory_uf.o
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/theory_uf'
>cd search && make 
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/search'
>Making dependencies for clause.cpp search_impl_base.cpp search.cpp search_fast.cpp search_theorem_producer.cpp search_sat.cpp search_simple.cpp variable.cpp circuit.cpp decision_engine.cpp decision_engine_dfs.cpp
>g++ -M -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include   clause.cpp search_impl_base.cpp search.cpp search_fast.cpp search_theorem_producer.cpp search_sat.cpp search_simple.cpp variable.cpp circuit.cpp decision_engine.cpp decision_engine_dfs.cpp >> /builddir/build/BUILD/cvc3-2.2/obj/search/x86_64-linux-gnu/Makefile.tmp
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/search'
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/search'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include   -c clause.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/search/x86_64-linux-gnu/clause.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include   -c search_impl_base.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/search/x86_64-linux-gnu/search_impl_base.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include   -c search.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/search/x86_64-linux-gnu/search.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include   -c search_theorem_producer.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/search/x86_64-linux-gnu/search_theorem_producer.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include   -c search_fast.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/search/x86_64-linux-gnu/search_fast.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include   -c search_sat.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/search/x86_64-linux-gnu/search_sat.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include   -c search_simple.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/search/x86_64-linux-gnu/search_simple.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include   -c variable.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/search/x86_64-linux-gnu/variable.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include   -c circuit.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/search/x86_64-linux-gnu/circuit.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include   -c decision_engine.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/search/x86_64-linux-gnu/decision_engine.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include   -c decision_engine_dfs.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/search/x86_64-linux-gnu/decision_engine_dfs.o'
>ar ruvs '/builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libsearch.a'  /builddir/build/BUILD/cvc3-2.2/obj/search/x86_64-linux-gnu/clause.o  /builddir/build/BUILD/cvc3-2.2/obj/search/x86_64-linux-gnu/search_impl_base.o  /builddir/build/BUILD/cvc3-2.2/obj/search/x86_64-linux-gnu/search.o  /builddir/build/BUILD/cvc3-2.2/obj/search/x86_64-linux-gnu/search_fast.o  /builddir/build/BUILD/cvc3-2.2/obj/search/x86_64-linux-gnu/search_theorem_producer.o  /builddir/build/BUILD/cvc3-2.2/obj/search/x86_64-linux-gnu/search_sat.o  /builddir/build/BUILD/cvc3-2.2/obj/search/x86_64-linux-gnu/search_simple.o  /builddir/build/BUILD/cvc3-2.2/obj/search/x86_64-linux-gnu/variable.o  /builddir/build/BUILD/cvc3-2.2/obj/search/x86_64-linux-gnu/circuit.o  /builddir/build/BUILD/cvc3-2.2/obj/search/x86_64-linux-gnu/decision_engine.o  /builddir/build/BUILD/cvc3-2.2/obj/search/x86_64-linux-gnu/decision_engine_dfs.o 
>ar: creating /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libsearch.a
>a - /builddir/build/BUILD/cvc3-2.2/obj/search/x86_64-linux-gnu/clause.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/search/x86_64-linux-gnu/search_impl_base.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/search/x86_64-linux-gnu/search.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/search/x86_64-linux-gnu/search_fast.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/search/x86_64-linux-gnu/search_theorem_producer.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/search/x86_64-linux-gnu/search_sat.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/search/x86_64-linux-gnu/search_simple.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/search/x86_64-linux-gnu/variable.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/search/x86_64-linux-gnu/circuit.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/search/x86_64-linux-gnu/decision_engine.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/search/x86_64-linux-gnu/decision_engine_dfs.o
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/search'
>cd parser && make 
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/parser'
>bison -d -y -o parsePL.cpp -p PL --debug -v PL.y
>bison -d -y -o parseLisp.cpp -p Lisp --debug -v Lisp.y
>bison -d -y -o parsesmtlib.cpp -p smtlib --debug -v smtlib.y
>conflicts: 3 shift/reduce
>PL.y:1531.24-1536.25: warning: rule useless in parser due to conflicts: AndExpr: AndExpr "AND" Expr
>PL.y:1549.25-1554.25: warning: rule useless in parser due to conflicts: OrExpr: OrExpr "OR" Expr
>flex  -I -PLisp -olexLisp.cpp Lisp.lex
>flex  -I -Psmtlib -olexsmtlib.cpp smtlib.lex
>flex  -I -PPL -olexPL.cpp PL.lex
>Making dependencies for parsePL.cpp lexPL.cpp parseLisp.cpp lexLisp.cpp parsesmtlib.cpp lexsmtlib.cpp parser.cpp
>g++ -M -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include -O0  parsePL.cpp lexPL.cpp parseLisp.cpp lexLisp.cpp parsesmtlib.cpp lexsmtlib.cpp parser.cpp >> /builddir/build/BUILD/cvc3-2.2/obj/parser/x86_64-linux-gnu/Makefile.tmp
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/parser'
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/parser'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include -O0  -c parsePL.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/parser/x86_64-linux-gnu/parsePL.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include -O0  -c lexPL.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/parser/x86_64-linux-gnu/lexPL.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include -O0  -c parseLisp.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/parser/x86_64-linux-gnu/parseLisp.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include -O0  -c lexLisp.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/parser/x86_64-linux-gnu/lexLisp.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include -O0  -c parsesmtlib.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/parser/x86_64-linux-gnu/parsesmtlib.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include -O0  -c lexsmtlib.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/parser/x86_64-linux-gnu/lexsmtlib.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include -O0  -c parser.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/parser/x86_64-linux-gnu/parser.o'
>ar ruvs '/builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libparser.a'  /builddir/build/BUILD/cvc3-2.2/obj/parser/x86_64-linux-gnu/parsePL.o  /builddir/build/BUILD/cvc3-2.2/obj/parser/x86_64-linux-gnu/lexPL.o  /builddir/build/BUILD/cvc3-2.2/obj/parser/x86_64-linux-gnu/parseLisp.o  /builddir/build/BUILD/cvc3-2.2/obj/parser/x86_64-linux-gnu/lexLisp.o  /builddir/build/BUILD/cvc3-2.2/obj/parser/x86_64-linux-gnu/parsesmtlib.o  /builddir/build/BUILD/cvc3-2.2/obj/parser/x86_64-linux-gnu/lexsmtlib.o  /builddir/build/BUILD/cvc3-2.2/obj/parser/x86_64-linux-gnu/parser.o 
>ar: creating /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libparser.a
>a - /builddir/build/BUILD/cvc3-2.2/obj/parser/x86_64-linux-gnu/parsePL.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/parser/x86_64-linux-gnu/lexPL.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/parser/x86_64-linux-gnu/parseLisp.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/parser/x86_64-linux-gnu/lexLisp.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/parser/x86_64-linux-gnu/parsesmtlib.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/parser/x86_64-linux-gnu/lexsmtlib.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/parser/x86_64-linux-gnu/parser.o
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/parser'
>cd translator && make 
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/translator'
>Making dependencies for translator.cpp
>g++ -M -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  translator.cpp >> /builddir/build/BUILD/cvc3-2.2/obj/translator/x86_64-linux-gnu/Makefile.tmp
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/translator'
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/translator'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c translator.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/translator/x86_64-linux-gnu/translator.o'
>ar ruvs '/builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libtranslator.a'  /builddir/build/BUILD/cvc3-2.2/obj/translator/x86_64-linux-gnu/translator.o 
>ar: creating /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libtranslator.a
>a - /builddir/build/BUILD/cvc3-2.2/obj/translator/x86_64-linux-gnu/translator.o
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/translator'
>cd vcl && make 
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/vcl'
>Making dependencies for vcl.cpp vc_cmd.cpp
>g++ -M -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  vcl.cpp vc_cmd.cpp >> /builddir/build/BUILD/cvc3-2.2/obj/vcl/x86_64-linux-gnu/Makefile.tmp
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/vcl'
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/vcl'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c vc_cmd.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/vcl/x86_64-linux-gnu/vc_cmd.o'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c vcl.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/vcl/x86_64-linux-gnu/vcl.o'
>ar ruvs '/builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libvcl.a'  /builddir/build/BUILD/cvc3-2.2/obj/vcl/x86_64-linux-gnu/vcl.o  /builddir/build/BUILD/cvc3-2.2/obj/vcl/x86_64-linux-gnu/vc_cmd.o 
>ar: creating /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libvcl.a
>a - /builddir/build/BUILD/cvc3-2.2/obj/vcl/x86_64-linux-gnu/vcl.o
>a - /builddir/build/BUILD/cvc3-2.2/obj/vcl/x86_64-linux-gnu/vc_cmd.o
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/vcl'
>cd c_interface && make 
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/c_interface'
>Making dependencies for c_interface.cpp
>g++ -M -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  c_interface.cpp >> /builddir/build/BUILD/cvc3-2.2/obj/c_interface/x86_64-linux-gnu/Makefile.tmp
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/c_interface'
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/c_interface'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include  -c c_interface.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/c_interface/x86_64-linux-gnu/c_interface.o'
>ar ruvs '/builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libc_interface.a'  /builddir/build/BUILD/cvc3-2.2/obj/c_interface/x86_64-linux-gnu/c_interface.o 
>ar: creating /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libc_interface.a
>a - /builddir/build/BUILD/cvc3-2.2/obj/c_interface/x86_64-linux-gnu/c_interface.o
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/c_interface'
>make /builddir/build/BUILD/cvc3-2.2/lib/libcvc3.so.2.1.1
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src'
>Building shared library /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libcvc3.so.2.1.1
>rm -rf /builddir/build/BUILD/cvc3-2.2/unpack_tmp
>/builddir/build/BUILD/cvc3-2.2/bin/unpack /builddir/build/BUILD/cvc3-2.2/unpack_tmp  /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libcvc_util.a  /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libcontext.a  /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libexpr.a  /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libtheorem.a  /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libsat.a  /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libtheory_core.a  /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libtheory_arith.a  /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libtheory_array.a  /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libtheory_bitvector.a  /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libtheory_datatype.a  /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libtheory_quant.a  /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libtheory_records.a  /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libtheory_simulate.a  /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libtheory_uf.a  /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libsearch.a  /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libparser.a  /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libtranslator.a  /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libvcl.a  /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libc_interface.a > UNPACKED
>Found 75 members in 19 libraries
>Unpacking cvc_util
>Unpacking context
>Unpacking expr
>Unpacking theorem
>Unpacking sat
>Unpacking theory_core
>Unpacking theory_arith
>Unpacking theory_array
>Unpacking theory_bitvector
>Unpacking theory_datatype
>Unpacking theory_quant
>Unpacking theory_records
>Unpacking theory_simulate
>Unpacking theory_uf
>Unpacking search
>Unpacking parser
>Unpacking translator
>Unpacking vcl
>Unpacking c_interface
>cat UNPACKED | xargs g++ -shared -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  \
>    -Wl,-soname,libcvc3.so.2 -o '/builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libcvc3.so.2.1.1' `` -lgmp 
>ldconfig -nv /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu
>/builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu:
>	libcvc3.so.2 -> libcvc3.so.2.1.1 (changed)
>ln -sf libcvc3.so.2.1.1 /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libcvc3.so.2.1
>ln -sf libcvc3.so.2.1.1 /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libcvc3.so.2
>ln -sf libcvc3.so.2.1.1 /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libcvc3.so
>ln -sf /builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu/libcvc3.so.2.1.1 '/builddir/build/BUILD/cvc3-2.2/lib//libcvc3.so.2.1.1'
>ldconfig -nv '/builddir/build/BUILD/cvc3-2.2/lib/'
>/builddir/build/BUILD/cvc3-2.2/lib:
>	libcvc3.so.2 -> libcvc3.so.2.1.1 (changed)
>ln -sf libcvc3.so.2.1.1 '/builddir/build/BUILD/cvc3-2.2/lib//libcvc3.so.2.1'
>ln -sf libcvc3.so.2.1.1 '/builddir/build/BUILD/cvc3-2.2/lib//libcvc3.so.2'
>ln -sf libcvc3.so.2.1.1 '/builddir/build/BUILD/cvc3-2.2/lib//libcvc3.so'
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src'
>cd cvc3 && make  VERSION=2.2
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/cvc3'
>Making dependencies for main.cpp
>g++ -M -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include -DVERSION=\"2.2\"  main.cpp >> /builddir/build/BUILD/cvc3-2.2/obj/cvc3/x86_64-linux-gnu/Makefile.tmp
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/cvc3'
>make[2]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/cvc3'
>make /builddir/build/BUILD/cvc3-2.2/bin/x86_64-linux-gnu/cvc3
>make[3]: Entering directory `/builddir/build/BUILD/cvc3-2.2/src/cvc3'
>g++ -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include -DVERSION=\"2.2\"  -c main.cpp -o '/builddir/build/BUILD/cvc3-2.2/obj/cvc3/x86_64-linux-gnu/main.o'
>g++  -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC  -I. -I/builddir/build/BUILD/cvc3-2.2/src/include -DVERSION=\"2.2\"  -o '/builddir/build/BUILD/cvc3-2.2/bin/x86_64-linux-gnu/cvc3'  /builddir/build/BUILD/cvc3-2.2/obj/cvc3/x86_64-linux-gnu/main.o \
>	 -L/builddir/build/BUILD/cvc3-2.2/lib/x86_64-linux-gnu -lcvc3 -lgmp 
>make[3]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/cvc3'
>ln -sf /builddir/build/BUILD/cvc3-2.2/bin/x86_64-linux-gnu/cvc3 /builddir/build/BUILD/cvc3-2.2/bin/cvc3
>make[2]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src/cvc3'
>make[1]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/src'
>cd /builddir/build/BUILD/cvc3-2.2/java; make  VERSION=2.2
>make[1]: Entering directory `/builddir/build/BUILD/cvc3-2.2/java'
>mkdir -p obj
>mkdir -p /builddir/build/BUILD/cvc3-2.2/java/lib/x86_64-linux-gnu
>mkdir -p /builddir/build/BUILD/cvc3-2.2/java/lib
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/JniUtils.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/Cvc3Exception.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/TypecheckException.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/SoundException.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/EvalException.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/CLException.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/ParserException.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/SmtlibException.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/DebugException.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/Embedded.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/EmbeddedManager.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/InputLanguage.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/QueryResult.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/SatResult.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/FormulaValue.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/Expr.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/ExprMut.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/ExprManager.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/ExprManagerMut.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/Type.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/TypeMut.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/Op.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/OpMut.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/Rational.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/RationalMut.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/Theorem.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/TheoremMut.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/Proof.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/ProofMut.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/Context.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/ContextMut.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/Flag.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/Flags.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/FlagsMut.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/Statistics.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/StatisticsMut.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/ValidityChecker.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/Test.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/TimeoutHandler.java
>/usr/lib/jvm/java/bin/javac  -Xlint -g -source 1.4 -sourcepath src \
>	-d obj src/cvc3/Cvc3.java
>/usr/lib/jvm/java/bin/javah -jni -force -classpath obj \
>	-o include/cvc3/EmbeddedManager.h cvc3.EmbeddedManager
>/usr/lib/jvm/java/bin/javah -jni -force -classpath obj \
>	-o include/cvc3/Expr.h cvc3.Expr
>/usr/lib/jvm/java/bin/javah -jni -force -classpath obj \
>	-o include/cvc3/ExprMut.h cvc3.ExprMut
>/usr/lib/jvm/java/bin/javah -jni -force -classpath obj \
>	-o include/cvc3/ExprManager.h cvc3.ExprManager
>/usr/lib/jvm/java/bin/javah -jni -force -classpath obj \
>	-o include/cvc3/Type.h cvc3.Type
>/usr/lib/jvm/java/bin/javah -jni -force -classpath obj \
>	-o include/cvc3/TypeMut.h cvc3.TypeMut
>/usr/lib/jvm/java/bin/javah -jni -force -classpath obj \
>	-o include/cvc3/Op.h cvc3.Op
>/usr/lib/jvm/java/bin/javah -jni -force -classpath obj \
>	-o include/cvc3/OpMut.h cvc3.OpMut
>/usr/lib/jvm/java/bin/javah -jni -force -classpath obj \
>	-o include/cvc3/Rational.h cvc3.Rational
>/usr/lib/jvm/java/bin/javah -jni -force -classpath obj \
>	-o include/cvc3/RationalMut.h cvc3.RationalMut
>/usr/lib/jvm/java/bin/javah -jni -force -classpath obj \
>	-o include/cvc3/Theorem.h cvc3.Theorem
>/usr/lib/jvm/java/bin/javah -jni -force -classpath obj \
>	-o include/cvc3/TheoremMut.h cvc3.TheoremMut
>/usr/lib/jvm/java/bin/javah -jni -force -classpath obj \
>	-o include/cvc3/Proof.h cvc3.Proof
>/usr/lib/jvm/java/bin/javah -jni -force -classpath obj \
>	-o include/cvc3/ProofMut.h cvc3.ProofMut
>/usr/lib/jvm/java/bin/javah -jni -force -classpath obj \
>	-o include/cvc3/Context.h cvc3.Context
>/usr/lib/jvm/java/bin/javah -jni -force -classpath obj \
>	-o include/cvc3/ContextMut.h cvc3.ContextMut
>/usr/lib/jvm/java/bin/javah -jni -force -classpath obj \
>	-o include/cvc3/Flag.h cvc3.Flag
>/usr/lib/jvm/java/bin/javah -jni -force -classpath obj \
>	-o include/cvc3/Flags.h cvc3.Flags
>/usr/lib/jvm/java/bin/javah -jni -force -classpath obj \
>	-o include/cvc3/FlagsMut.h cvc3.FlagsMut
>/usr/lib/jvm/java/bin/javah -jni -force -classpath obj \
>	-o include/cvc3/Statistics.h cvc3.Statistics
>/usr/lib/jvm/java/bin/javah -jni -force -classpath obj \
>	-o include/cvc3/StatisticsMut.h cvc3.StatisticsMut
>/usr/lib/jvm/java/bin/javah -jni -force -classpath obj \
>	-o include/cvc3/ValidityChecker.h cvc3.ValidityChecker
>g++  -I/usr/lib/jvm/java/include -I/usr/lib/jvm/java/include/linux -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -m64 -fPIC -O2 -c \
>	-I ../src/include -I include/cvc3/ \
>	-o obj/cvc3/JniUtils.o src/cvc3/JniUtils.cpp
>./create_impl.py \
>	include/cvc3/EmbeddedManager.h \
>	src/cvc3/EmbeddedManager_impl.cpp \
>	src/cvc3/EmbeddedManager.cpp
>/bin/bash: line 1: ./create_impl.py: Permission denied
>make[1]: *** [EmbeddedManager.cpp] Error 126
>make[1]: *** Waiting for unfinished jobs....
>src/cvc3/JniUtils.cpp: In function '_jstring* Java_cvc3_JniUtils::toJava(JNIEnv*, CVC3::InputLanguage)':
>src/cvc3/JniUtils.cpp:73: warning: enumeration value 'AST_LANG' not handled in switch
>src/cvc3/JniUtils.cpp:73: warning: enumeration value 'SIMPLIFY_LANG' not handled in switch
>src/cvc3/JniUtils.cpp:73: warning: enumeration value 'TPTP_LANG' not handled in switch
>src/cvc3/JniUtils.cpp: In function '_jobjectArray* Java_cvc3_JniUtils::toJavaV(JNIEnv*, const std::vector<std::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::allocator<std::basic_string<char, std::char_traits<char>, std::allocator<char> > > >&)':
>src/cvc3/JniUtils.cpp:159: warning: comparison between signed and unsigned integer expressions
>src/cvc3/JniUtils.cpp: In function 'CVC3::InputLanguage Java_cvc3_JniUtils::toCppInputLanguage(JNIEnv*, const std::string&)':
>src/cvc3/JniUtils.cpp:92: warning: control reaches end of non-void function
>src/cvc3/JniUtils.cpp: In function '_jstring* Java_cvc3_JniUtils::toJava(JNIEnv*, CVC3::InputLanguage)':
>src/cvc3/JniUtils.cpp:80: warning: control reaches end of non-void function
>src/cvc3/JniUtils.cpp: In function '_jstring* Java_cvc3_JniUtils::toJava(JNIEnv*, CVC3::FormulaValue)':
>src/cvc3/JniUtils.cpp:70: warning: control reaches end of non-void function
>make[1]: Leaving directory `/builddir/build/BUILD/cvc3-2.2/java'
>make: *** [build] Error 2
>error: Bad exit status from /var/tmp/rpm-tmp.jvwh9m (%build)
>RPM build errors:
>    Bad exit status from /var/tmp/rpm-tmp.jvwh9m (%build)
>Child returncode was: 1
>EXCEPTION: Command failed. See logs for output.
> # ['bash', '--login', '-c', 'rpmbuild -bb --target x86_64 --nodeps builddir/build/SPECS/cvc3.spec']
>Traceback (most recent call last):
>  File "/usr/lib/python2.6/site-packages/mock/trace_decorator.py", line 70, in trace
>    result = func(*args, **kw)
>  File "/usr/lib/python2.6/site-packages/mock/util.py", line 333, in do
>    raise mock.exception.Error, ("Command failed. See logs for output.\n # %s" % (command,), child.returncode)
>Error: Command failed. See logs for output.
> # ['bash', '--login', '-c', 'rpmbuild -bb --target x86_64 --nodeps builddir/build/SPECS/cvc3.spec']
>LEAVE do --> EXCEPTION RAISED
>

Actions: View

Attachments on bug 599887: 420257 | 420258 | 420259 | 420260 | 420261 | 420262