=> Building math/cvc3 Started : Friday, 8 MAR 2019 at 18:00:23 UTC Platform: 5.5-DEVELOPMENT DragonFly v5.5.0.192.g15ae7f0-DEVELOPMENT #34: Tue Feb 19 09:07:07 PST 2019 root@pkgbox64.dragonflybsd.org:/usr/obj/usr/src/sys/X86_64_GENERIC x86_64 -------------------------------------------------- -- Environment -------------------------------------------------- UNAME_r=5.5-SYNTH UNAME_m=x86_64 UNAME_p=x86_64 UNAME_v=DragonFly 5.5-SYNTH UNAME_s=DragonFly PATH=/sbin:/bin:/usr/sbin:/usr/bin:/usr/local/sbin:/usr/local/bin SSL_NO_VERIFY_PEER=1 TERM=dumb PKG_CACHEDIR=/var/cache/pkg8 PKG_DBDIR=/var/db/pkg8 PORTSDIR=/xports LANG=C HOME=/root USER=root -------------------------------------------------- -- Options -------------------------------------------------- -------------------------------------------------- -- CONFIGURE_ENV -------------------------------------------------- MAKE=gmake ac_cv_path_PERL=/usr/local/bin/perl ac_cv_path_PERL_PATH=/usr/local/bin/perl PERL_USE_UNSAFE_INC=1 XDG_DATA_HOME=/construction/math/cvc3 XDG_CONFIG_HOME=/construction/math/cvc3 HOME=/construction/math/cvc3 TMPDIR="/tmp" PATH=/construction/math/cvc3/.bin:/sbin:/bin:/usr/sbin:/usr/bin:/usr/local/sbin:/usr/local/bin SHELL=/bin/sh CONFIG_SHELL=/bin/sh CCVER=gcc80 CONFIG_SITE=/xports/Templates/config.site lt_cv_sys_max_cmd_len=262144 -------------------------------------------------- -- CONFIGURE_ARGS -------------------------------------------------- --enable-dynamic --with-arith=gmp --with-build=optimized --with-extra-includes=/usr/local/include --with-extra-libs=/usr/local/lib --prefix=/usr/local ${_LATE_CONFIGURE_ARGS} -------------------------------------------------- -- MAKE_ENV -------------------------------------------------- PERL_USE_UNSAFE_INC=1 XDG_DATA_HOME=/construction/math/cvc3 XDG_CONFIG_HOME=/construction/math/cvc3 HOME=/construction/math/cvc3 TMPDIR="/tmp" PATH=/construction/math/cvc3/.bin:/sbin:/bin:/usr/sbin:/usr/bin:/usr/local/sbin:/usr/local/bin NO_PIE=yes MK_DEBUG_FILES=no MK_KERNEL_SYMBOLS=no SHELL=/bin/sh NO_LINT=YES CCVER=gcc80 PREFIX=/usr/local LOCALBASE=/usr/local NOPROFILE=1 CC="gcc" CFLAGS="-pipe -O2 -fno-strict-aliasing " CPP="cpp" CPPFLAGS="" LDFLAGS=" " LIBS="" CXX="g++" CXXFLAGS=" -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 " MANPREFIX="/usr/local" BSD_INSTALL_PROGRAM="install -s -m 555" BSD_INSTALL_LIB="install -s -m 0644" BSD_INSTALL_SCRIPT="install -m 555" BSD_INSTALL_DATA="install -m 0644" BSD_INSTALL_MAN="install -m 444" -------------------------------------------------- -- MAKE_ARGS -------------------------------------------------- DESTDIR=/construction/math/cvc3/stage -------------------------------------------------- -- PLIST_SUB -------------------------------------------------- OSREL=5.5 PREFIX=%D LOCALBASE=/usr/local RESETPREFIX=/usr/local LIB32DIR=lib PERL_VERSION=5.28.1 PERL_VER=5.28 PERL5_MAN1=lib/perl5/site_perl/man/man1 PERL5_MAN3=lib/perl5/site_perl/man/man3 SITE_PERL=lib/perl5/site_perl SITE_ARCH=lib/perl5/site_perl/mach/5.28 PROFILE="@comment " DOCSDIR="share/doc/cvc3" EXAMPLESDIR="share/examples/cvc3" DATADIR="share/cvc3" WWWDIR="www/cvc3" ETCDIR="etc/cvc3" -------------------------------------------------- -- SUB_LIST -------------------------------------------------- PREFIX=/usr/local LOCALBASE=/usr/local DATADIR=/usr/local/share/cvc3 DOCSDIR=/usr/local/share/doc/cvc3 EXAMPLESDIR=/usr/local/share/examples/cvc3 WWWDIR=/usr/local/www/cvc3 ETCDIR=/usr/local/etc/cvc3 -------------------------------------------------- -- /etc/make.conf -------------------------------------------------- SYNTHPROFILE=Release-BE USE_PACKAGE_DEPENDS_ONLY=yes PACKAGE_BUILDING=yes BATCH=yes PKG_CREATE_VERBOSE=yes PORTSDIR=/xports DISTDIR=/distfiles WRKDIRPREFIX=/construction PORT_DBDIR=/options PACKAGES=/packages MAKE_JOBS_NUMBER_LIMIT=5 LICENSES_ACCEPTED= NONE HAVE_COMPAT_IA32_KERN= CONFIGURE_MAX_CMD_LEN=262144 _PERL5_FROM_BIN=5.26.2 _ALTCCVERSION_921dbbb2=none _OBJC_ALTCCVERSION_921dbbb2=none _SMP_CPUS=8 UID=0 ARCH=x86_64 OPSYS=DragonFly DFLYVERSION=500500 OSVERSION=9999999 OSREL=5.5 _OSRELEASE=5.5-SYNTH PYTHONBASE=/usr/local _PKG_CHECKED=1 -------------------------------------------------------------------------------- -- Phase: check-sanity -------------------------------------------------------------------------------- -------------------------------------------------------------------------------- -- Phase: pkg-depends -------------------------------------------------------------------------------- ===> cvc3-2.4.1_6 depends on file: /usr/local/sbin/pkg - not found ===> Installing existing package /packages/All/pkg-1.10.5_5.txz Installing pkg-1.10.5_5... Extracting pkg-1.10.5_5: .......... done ===> cvc3-2.4.1_6 depends on file: /usr/local/sbin/pkg - found ===> Returning to build of cvc3-2.4.1_6 -------------------------------------------------------------------------------- -- Phase: fetch-depends -------------------------------------------------------------------------------- -------------------------------------------------------------------------------- -- Phase: fetch -------------------------------------------------------------------------------- ===> Fetching all distfiles required by cvc3-2.4.1_6 for building -------------------------------------------------------------------------------- -- Phase: checksum -------------------------------------------------------------------------------- ===> Fetching all distfiles required by cvc3-2.4.1_6 for building => SHA256 Checksum OK for cvc3-2.4.1.tar.gz. -------------------------------------------------------------------------------- -- Phase: extract-depends -------------------------------------------------------------------------------- -------------------------------------------------------------------------------- -- Phase: extract -------------------------------------------------------------------------------- ===> Fetching all distfiles required by cvc3-2.4.1_6 for building ===> Extracting for cvc3-2.4.1_6 => SHA256 Checksum OK for cvc3-2.4.1.tar.gz. -------------------------------------------------------------------------------- -- Phase: patch-depends -------------------------------------------------------------------------------- -------------------------------------------------------------------------------- -- Phase: patch -------------------------------------------------------------------------------- ===> Patching for cvc3-2.4.1_6 ===> Applying ports patches for cvc3-2.4.1_6 /usr/bin/sed -i.bak -e 's,/bin/bash,/bin/sh,' /construction/math/cvc3/cvc3-2.4.1/Makefile.std /usr/bin/sed -i.bak -e 's,.*$(LDCONFIG).*,,' /construction/math/cvc3/cvc3-2.4.1/src/Makefile -------------------------------------------------------------------------------- -- Phase: build-depends -------------------------------------------------------------------------------- ===> cvc3-2.4.1_6 depends on executable: bison - not found ===> Installing existing package /packages/All/bison-3.3.2,1.txz Installing bison-3.3.2,1... `-- Installing gettext-runtime-0.19.8.1_2... | `-- Installing indexinfo-0.3.1... | `-- Extracting indexinfo-0.3.1: .... done `-- Extracting gettext-runtime-0.19.8.1_2: .......... done `-- Installing m4-1.4.18_1,1... `-- Extracting m4-1.4.18_1,1: .......... done Extracting bison-3.3.2,1: .......... done ===> cvc3-2.4.1_6 depends on executable: bison - found ===> Returning to build of cvc3-2.4.1_6 ===> cvc3-2.4.1_6 depends on executable: gmake - not found ===> Installing existing package /packages/All/gmake-4.2.1_3.txz Installing gmake-4.2.1_3... Extracting gmake-4.2.1_3: .......... done ===> cvc3-2.4.1_6 depends on executable: gmake - found ===> Returning to build of cvc3-2.4.1_6 ===> cvc3-2.4.1_6 depends on package: perl5>=5.28.r1<5.29 - not found ===> Installing existing package /packages/All/perl5-5.28.1.txz Installing perl5-5.28.1... Extracting perl5-5.28.1: .......... done Message from perl5-5.28.1: The /usr/bin/perl symlink has been removed starting with Perl 5.20. For shebangs, you should either use: #!/usr/local/bin/perl or #!/usr/bin/env perl The first one will only work if you have a /usr/local/bin/perl, the second will work as long as perl is in PATH. ===> cvc3-2.4.1_6 depends on package: perl5>=5.28.r1<5.29 - found ===> Returning to build of cvc3-2.4.1_6 -------------------------------------------------------------------------------- -- Phase: lib-depends -------------------------------------------------------------------------------- ===> cvc3-2.4.1_6 depends on shared library: libgmp.so - not found ===> Installing existing package /packages/All/gmp-6.1.2_1.txz Installing gmp-6.1.2_1... Extracting gmp-6.1.2_1: .......... done ===> cvc3-2.4.1_6 depends on shared library: libgmp.so - found (/usr/local/lib/libgmp.so) ===> Returning to build of cvc3-2.4.1_6 -------------------------------------------------------------------------------- -- Phase: configure -------------------------------------------------------------------------------- ===> Configuring for cvc3-2.4.1_6 configure: loading site script /xports/Templates/config.site checking whether the C++ compiler works... yes checking for C++ compiler default output file name... a.out checking for suffix of executables... checking whether we are cross compiling... no checking for suffix of object files... o checking whether we are using the GNU C++ compiler... yes checking whether g++ accepts -g... yes checking how to run the C++ preprocessor... g++ -E checking for ar... ar checking build system type... x86_64-portbld-dragonfly5.5 checking host system type... x86_64-portbld-dragonfly5.5 checking for install... /usr/bin/install -c checking for ldconfig... /sbin/ldconfig checking for time... /usr/bin/time checking for perl... (cached) /usr/local/bin/perl checking for bison... bison -y checking for flex... flex checking lex output file root... lex.yy checking lex library... none needed checking whether yytext is a pointer... no checking for compiler version (g++ --version)... 8.1 checking for gmp... yes checking vector usability... yes checking vector presence... yes checking for vector... yes checking list usability... yes checking list presence... yes checking for list... yes checking deque usability... yes checking deque presence... yes checking for deque... yes checking set usability... yes checking set presence... yes checking for set... yes checking string usability... yes checking string presence... yes checking for string... yes checking cstdlib usability... yes checking cstdlib presence... yes checking for cstdlib... yes checking cstdio usability... yes checking cstdio presence... yes checking for cstdio... yes checking functional usability... yes checking functional presence... yes checking for functional... yes checking algorithm usability... yes checking algorithm presence... yes checking for algorithm... yes checking for doxygen... no checking for doxytag... no checking for fig2dev... no checking for dot... NO checking for etags... no checking for ebrowse... no configure: creating ./config.status config.status: creating Makefile.local config.status: creating LICENSE config.status: creating src/cvc3.pc config.status: creating bin/unpack config.status: creating bin/run_tests config.status: creating bin/cvc2smt config.status: creating doc/Doxyfile config.status: creating doc/Makefile CVC3 is configured successfully. Platform: x86_64-dragonfly5.5 Version: 2.4.1 Computer arithmetic: GMP Run ./configure --help for additional configuration options. Type 'make' to compile CVC3. *** CVC3 is configured to compile using shared libraries. *** Type "make ld_sh" for bash shells or "make ld_csh" for csh shells *** to see how to set LD_LIBRARY_PATH appropriately. To use static *** libraries and executables instead, run: *** ./configure --enable-static -------------------------------------------------------------------------------- -- Phase: build -------------------------------------------------------------------------------- ===> Building for cvc3-2.4.1_6 gmake[1]: Entering directory '/construction/math/cvc3/cvc3-2.4.1' cd /construction/math/cvc3/cvc3-2.4.1/src; gmake VERSION=2.4.1 gmake[2]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src' cd util && gmake gmake[3]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/util' Making dependencies for debug.cpp statistics.cpp rational.cpp rational-native.cpp rational-gmp.cpp g++ -M -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DRATIONAL_GMP -I/usr/local/include debug.cpp statistics.cpp rational.cpp rational-native.cpp rational-gmp.cpp >> /construction/math/cvc3/cvc3-2.4.1/obj/util/x86_64-dragonfly5.5/Makefile.tmp g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DRATIONAL_GMP -I/usr/local/include -c debug.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/util/x86_64-dragonfly5.5/debug.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DRATIONAL_GMP -I/usr/local/include -c rational-native.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/util/x86_64-dragonfly5.5/rational-native.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DRATIONAL_GMP -I/usr/local/include -c rational.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/util/x86_64-dragonfly5.5/rational.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DRATIONAL_GMP -I/usr/local/include -c statistics.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/util/x86_64-dragonfly5.5/statistics.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DRATIONAL_GMP -I/usr/local/include -c rational-gmp.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/util/x86_64-dragonfly5.5/rational-gmp.o' ar ruvs '/construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libcvc_util.a' /construction/math/cvc3/cvc3-2.4.1/obj/util/x86_64-dragonfly5.5/debug.o /construction/math/cvc3/cvc3-2.4.1/obj/util/x86_64-dragonfly5.5/statistics.o /construction/math/cvc3/cvc3-2.4.1/obj/util/x86_64-dragonfly5.5/rational.o /construction/math/cvc3/cvc3-2.4.1/obj/util/x86_64-dragonfly5.5/rational-native.o /construction/math/cvc3/cvc3-2.4.1/obj/util/x86_64-dragonfly5.5/rational-gmp.o /usr/libexec/binutils227/elf/ar: `u' modifier ignored since `D' is the default (see `U') /usr/libexec/binutils227/elf/ar: creating /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libcvc_util.a a - /construction/math/cvc3/cvc3-2.4.1/obj/util/x86_64-dragonfly5.5/debug.o a - /construction/math/cvc3/cvc3-2.4.1/obj/util/x86_64-dragonfly5.5/statistics.o a - /construction/math/cvc3/cvc3-2.4.1/obj/util/x86_64-dragonfly5.5/rational.o a - /construction/math/cvc3/cvc3-2.4.1/obj/util/x86_64-dragonfly5.5/rational-native.o a - /construction/math/cvc3/cvc3-2.4.1/obj/util/x86_64-dragonfly5.5/rational-gmp.o gmake[3]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/util' cd context && gmake gmake[3]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/context' Making dependencies for context.cpp cdflags.cpp g++ -M -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include context.cpp cdflags.cpp >> /construction/math/cvc3/cvc3-2.4.1/obj/context/x86_64-dragonfly5.5/Makefile.tmp g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c context.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/context/x86_64-dragonfly5.5/context.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c cdflags.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/context/x86_64-dragonfly5.5/cdflags.o' ar ruvs '/construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libcontext.a' /construction/math/cvc3/cvc3-2.4.1/obj/context/x86_64-dragonfly5.5/context.o /construction/math/cvc3/cvc3-2.4.1/obj/context/x86_64-dragonfly5.5/cdflags.o /usr/libexec/binutils227/elf/ar: `u' modifier ignored since `D' is the default (see `U') /usr/libexec/binutils227/elf/ar: creating /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libcontext.a a - /construction/math/cvc3/cvc3-2.4.1/obj/context/x86_64-dragonfly5.5/context.o a - /construction/math/cvc3/cvc3-2.4.1/obj/context/x86_64-dragonfly5.5/cdflags.o gmake[3]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/context' cd expr && gmake gmake[3]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/expr' Making dependencies for expr.cpp expr_manager.cpp expr_stream.cpp expr_value.cpp expr_op.cpp g++ -M -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include expr.cpp expr_manager.cpp expr_stream.cpp expr_value.cpp expr_op.cpp >> /construction/math/cvc3/cvc3-2.4.1/obj/expr/x86_64-dragonfly5.5/Makefile.tmp g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c expr.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/expr/x86_64-dragonfly5.5/expr.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c expr_manager.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/expr/x86_64-dragonfly5.5/expr_manager.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c expr_stream.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/expr/x86_64-dragonfly5.5/expr_stream.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c expr_value.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/expr/x86_64-dragonfly5.5/expr_value.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c expr_op.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/expr/x86_64-dragonfly5.5/expr_op.o' ar ruvs '/construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libexpr.a' /construction/math/cvc3/cvc3-2.4.1/obj/expr/x86_64-dragonfly5.5/expr.o /construction/math/cvc3/cvc3-2.4.1/obj/expr/x86_64-dragonfly5.5/expr_manager.o /construction/math/cvc3/cvc3-2.4.1/obj/expr/x86_64-dragonfly5.5/expr_stream.o /construction/math/cvc3/cvc3-2.4.1/obj/expr/x86_64-dragonfly5.5/expr_value.o /construction/math/cvc3/cvc3-2.4.1/obj/expr/x86_64-dragonfly5.5/expr_op.o /usr/libexec/binutils227/elf/ar: `u' modifier ignored since `D' is the default (see `U') /usr/libexec/binutils227/elf/ar: creating /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libexpr.a a - /construction/math/cvc3/cvc3-2.4.1/obj/expr/x86_64-dragonfly5.5/expr.o a - /construction/math/cvc3/cvc3-2.4.1/obj/expr/x86_64-dragonfly5.5/expr_manager.o a - /construction/math/cvc3/cvc3-2.4.1/obj/expr/x86_64-dragonfly5.5/expr_stream.o a - /construction/math/cvc3/cvc3-2.4.1/obj/expr/x86_64-dragonfly5.5/expr_value.o a - /construction/math/cvc3/cvc3-2.4.1/obj/expr/x86_64-dragonfly5.5/expr_op.o gmake[3]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/expr' cd theorem && gmake gmake[3]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/theorem' Making dependencies for assumptions.cpp theorem.cpp theorem_manager.cpp theorem_producer.cpp common_theorem_producer.cpp g++ -M -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include assumptions.cpp theorem.cpp theorem_manager.cpp theorem_producer.cpp common_theorem_producer.cpp >> /construction/math/cvc3/cvc3-2.4.1/obj/theorem/x86_64-dragonfly5.5/Makefile.tmp g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c assumptions.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/theorem/x86_64-dragonfly5.5/assumptions.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c theorem.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/theorem/x86_64-dragonfly5.5/theorem.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c theorem_manager.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/theorem/x86_64-dragonfly5.5/theorem_manager.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c theorem_producer.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/theorem/x86_64-dragonfly5.5/theorem_producer.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c common_theorem_producer.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/theorem/x86_64-dragonfly5.5/common_theorem_producer.o' In file included from common_theorem_producer.h:34, from common_theorem_producer.cpp:27: common_theorem_producer.cpp: In member function 'virtual CVC3::Theorem CVC3::CommonTheoremProducer::contradictionRule(const CVC3::Theorem&, const CVC3::Theorem&)': common_theorem_producer.cpp:565:30: warning: logical not is only applied to the left hand side of comparison [-Wlogical-not-parentheses] CHECK_SOUND(!e.getExpr() == not_e.getExpr(), ^~ /construction/math/cvc3/cvc3-2.4.1/src/include/theorem_producer.h:83:39: note: in definition of macro 'CHECK_SOUND' #define CHECK_SOUND(cond, msg) { if(!(cond)) \ ^~~~ common_theorem_producer.cpp:565:17: note: add parentheses around left hand side expression to silence this warning CHECK_SOUND(!e.getExpr() == not_e.getExpr(), ^~~~~~~~~~~~ /construction/math/cvc3/cvc3-2.4.1/src/include/theorem_producer.h:83:39: note: in definition of macro 'CHECK_SOUND' #define CHECK_SOUND(cond, msg) { if(!(cond)) \ ^~~~ ar ruvs '/construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libtheorem.a' /construction/math/cvc3/cvc3-2.4.1/obj/theorem/x86_64-dragonfly5.5/assumptions.o /construction/math/cvc3/cvc3-2.4.1/obj/theorem/x86_64-dragonfly5.5/theorem.o /construction/math/cvc3/cvc3-2.4.1/obj/theorem/x86_64-dragonfly5.5/theorem_manager.o /construction/math/cvc3/cvc3-2.4.1/obj/theorem/x86_64-dragonfly5.5/theorem_producer.o /construction/math/cvc3/cvc3-2.4.1/obj/theorem/x86_64-dragonfly5.5/common_theorem_producer.o /usr/libexec/binutils227/elf/ar: `u' modifier ignored since `D' is the default (see `U') /usr/libexec/binutils227/elf/ar: creating /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libtheorem.a a - /construction/math/cvc3/cvc3-2.4.1/obj/theorem/x86_64-dragonfly5.5/assumptions.o a - /construction/math/cvc3/cvc3-2.4.1/obj/theorem/x86_64-dragonfly5.5/theorem.o a - /construction/math/cvc3/cvc3-2.4.1/obj/theorem/x86_64-dragonfly5.5/theorem_manager.o a - /construction/math/cvc3/cvc3-2.4.1/obj/theorem/x86_64-dragonfly5.5/theorem_producer.o a - /construction/math/cvc3/cvc3-2.4.1/obj/theorem/x86_64-dragonfly5.5/common_theorem_producer.o gmake[3]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/theorem' cd sat && gmake gmake[3]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/sat' Making dependencies for xchaff.cpp xchaff_dbase.cpp xchaff_solver.cpp xchaff_utils.cpp 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 -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DDPLL_BASIC -I/usr/local/include xchaff.cpp xchaff_dbase.cpp xchaff_solver.cpp xchaff_utils.cpp 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 >> /construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/Makefile.tmp g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DDPLL_BASIC -I/usr/local/include -c xchaff_dbase.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/xchaff_dbase.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DDPLL_BASIC -I/usr/local/include -c xchaff.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/xchaff.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DDPLL_BASIC -I/usr/local/include -c xchaff_utils.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/xchaff_utils.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DDPLL_BASIC -I/usr/local/include -c xchaff_solver.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/xchaff_solver.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DDPLL_BASIC -I/usr/local/include -c cnf.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/cnf.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DDPLL_BASIC -I/usr/local/include -c cnf_manager.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/cnf_manager.o' In file included from xchaff.cpp:11: xchaff.h: In member function 'virtual SatSolver::Var Xchaff::GetNextVar(SatSolver::Var)': xchaff.h:48:4: warning: this 'if' clause does not guard... [-Wmisleading-indentation] if (var.id != _solver->num_variables()) v.id = var.id+1; return v; } ^~ xchaff.h:48:61: note: ...this statement, but the latter is misleadingly indented as if it were guarded by the 'if' if (var.id != _solver->num_variables()) v.id = var.id+1; return v; } ^~~~~~ g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DDPLL_BASIC -I/usr/local/include -c cnf_theorem_producer.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/cnf_theorem_producer.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DDPLL_BASIC -I/usr/local/include -c dpllt_basic.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/dpllt_basic.o' dpllt_basic.cpp: In member function 'void SAT::DPLLTBasic::handle_result(SatSolver::SATStatus)': dpllt_basic.cpp:172:16: warning: variable 'result' set but not used [-Wunused-but-set-variable] const char * result = "UNKNOWN"; ^~~~~~ g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DDPLL_BASIC -I/usr/local/include -c sat_api.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/sat_api.o' sat_api.cpp: In member function 'void SatSolver::PrintStatistics(std::ostream&)': sat_api.cpp:29:3: warning: this 'if' clause does not guard... [-Wmisleading-indentation] if (val != -1) ^~ sat_api.cpp:32:5: note: ...this statement, but the latter is misleadingly indented as if it were guarded by the 'if' os << "Number of Clauses\t\t\t" << NumClauses() << endl; ^~ g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DDPLL_BASIC -I/usr/local/include -c dpllt_minisat.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/dpllt_minisat.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DDPLL_BASIC -I/usr/local/include -c minisat_types.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/minisat_types.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DDPLL_BASIC -I/usr/local/include -c minisat_derivation.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/minisat_derivation.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DDPLL_BASIC -I/usr/local/include -c minisat_solver.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/minisat_solver.o' ar ruvs '/construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libsat.a' /construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/xchaff.o /construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/xchaff_dbase.o /construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/xchaff_solver.o /construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/xchaff_utils.o /construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/cnf.o /construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/cnf_manager.o /construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/cnf_theorem_producer.o /construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/dpllt_basic.o /construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/sat_api.o /construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/dpllt_minisat.o /construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/minisat_types.o /construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/minisat_derivation.o /construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/minisat_solver.o /usr/libexec/binutils227/elf/ar: `u' modifier ignored since `D' is the default (see `U') /usr/libexec/binutils227/elf/ar: creating /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libsat.a a - /construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/xchaff.o a - /construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/xchaff_dbase.o a - /construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/xchaff_solver.o a - /construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/xchaff_utils.o a - /construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/cnf.o a - /construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/cnf_manager.o a - /construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/cnf_theorem_producer.o a - /construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/dpllt_basic.o a - /construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/sat_api.o a - /construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/dpllt_minisat.o a - /construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/minisat_types.o a - /construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/minisat_derivation.o a - /construction/math/cvc3/cvc3-2.4.1/obj/sat/x86_64-dragonfly5.5/minisat_solver.o gmake[3]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/sat' cd theory_core && gmake gmake[3]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/theory_core' Making dependencies for theory.cpp theory_core.cpp core_theorem_producer.cpp expr_transform.cpp bryant.cpp g++ -M -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include theory.cpp theory_core.cpp core_theorem_producer.cpp expr_transform.cpp bryant.cpp >> /construction/math/cvc3/cvc3-2.4.1/obj/theory_core/x86_64-dragonfly5.5/Makefile.tmp g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c theory.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/theory_core/x86_64-dragonfly5.5/theory.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c theory_core.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/theory_core/x86_64-dragonfly5.5/theory_core.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c core_theorem_producer.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/theory_core/x86_64-dragonfly5.5/core_theorem_producer.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c expr_transform.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/theory_core/x86_64-dragonfly5.5/expr_transform.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c bryant.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/theory_core/x86_64-dragonfly5.5/bryant.o' theory_core.cpp: In constructor 'CVC3::TheoryCore::TheoryCore(CVC3::ContextManager*, CVC3::ExprManager*, CVC3::TheoremManager*, CVC3::Translator*, const CVC3::CLFlags&, CVC3::Statistics&)': theory_core.cpp:725:22: warning: converting 'false' to pointer type 'const bool*' [-Wconversion-null] d_coreSatAPI(NULL) ^ bryant.cpp: In member function 'void CVC3::ExprTransform::GetPEqs(const CVC3::Expr&, CVC3::ExprTransform::B_name_map&, std::set&, std::set&, CVC3::ExprTransform::T_generator_map&, std::set&)': bryant.cpp:402:5: warning: this 'if' clause does not guard... [-Wmisleading-indentation] if (!SeenBefore.insert(e).second) ^~ bryant.cpp:404:2: note: ...this statement, but the latter is misleadingly indented as if it were guarded by the 'if' if (e.isEq()) { ^~ bryant.cpp: In member function 'CVC3::Expr CVC3::ExprTransform::ConstrainedConstraints(std::set&, CVC3::ExprTransform::T_generator_map&, CVC3::ExprTransform::B_name_map&, CVC3::ExprTransform::B_Term_map&, std::set&, std::set&, std::set&)': bryant.cpp:452:3: warning: this 'else' clause does not guard... [-Wmisleading-indentation] else ^~~~ bryant.cpp:454:4: note: ...this statement, but the latter is misleadingly indented as if it were guarded by the 'else' for (set::iterator j = (*f).second->begin(); j != (*f).second->end(); j++) { ^~~ bryant.cpp:470:17: warning: logical not is only applied to the left hand side of comparison [-Wlogical-not-parentheses] if (!Value == Temp) ^~ bryant.cpp:470:10: note: add parentheses around left hand side expression to silence this warning if (!Value == Temp) ^~~~~~ ( ) theory_core.cpp: In member function 'bool CVC3::TheoryCore::refineCounterExample(CVC3::Theorem&)': theory_core.cpp:3419:3: warning: this 'if' clause does not guard... [-Wmisleading-indentation] if(d_theories[i] != this) ^~ theory_core.cpp:3421:4: note: ...this statement, but the latter is misleadingly indented as if it were guarded by the 'if' if(inconsistent()) { ^~ In file included from /construction/math/cvc3/cvc3-2.4.1/src/include/expr_stream.h:36, from /construction/math/cvc3/cvc3-2.4.1/src/include/theory.h:25, from /construction/math/cvc3/cvc3-2.4.1/src/include/theory_core.h:25, from theory.cpp:22: /construction/math/cvc3/cvc3-2.4.1/src/include/expr.h: In member function 'CVC3::Theory* CVC3::Theory::theoryOf(const CVC3::Expr&)': /construction/math/cvc3/cvc3-2.4.1/src/include/expr.h:1017:17: warning: '' may be used uninitialized in this function [-Wmaybe-uninitialized] return getKind() == APPLY; } ~~~~~~~^~ /construction/math/cvc3/cvc3-2.4.1/src/include/expr.h: In member function 'CVC3::Theory* CVC3::Theory::theoryOf(const CVC3::Type&)': /construction/math/cvc3/cvc3-2.4.1/src/include/expr.h:1017:17: warning: '' is used uninitialized in this function [-Wuninitialized] return getKind() == APPLY; } ~~~~~~~^~ ar ruvs '/construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libtheory_core.a' /construction/math/cvc3/cvc3-2.4.1/obj/theory_core/x86_64-dragonfly5.5/theory.o /construction/math/cvc3/cvc3-2.4.1/obj/theory_core/x86_64-dragonfly5.5/theory_core.o /construction/math/cvc3/cvc3-2.4.1/obj/theory_core/x86_64-dragonfly5.5/core_theorem_producer.o /construction/math/cvc3/cvc3-2.4.1/obj/theory_core/x86_64-dragonfly5.5/expr_transform.o /construction/math/cvc3/cvc3-2.4.1/obj/theory_core/x86_64-dragonfly5.5/bryant.o /usr/libexec/binutils227/elf/ar: `u' modifier ignored since `D' is the default (see `U') /usr/libexec/binutils227/elf/ar: creating /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libtheory_core.a a - /construction/math/cvc3/cvc3-2.4.1/obj/theory_core/x86_64-dragonfly5.5/theory.o a - /construction/math/cvc3/cvc3-2.4.1/obj/theory_core/x86_64-dragonfly5.5/theory_core.o a - /construction/math/cvc3/cvc3-2.4.1/obj/theory_core/x86_64-dragonfly5.5/core_theorem_producer.o a - /construction/math/cvc3/cvc3-2.4.1/obj/theory_core/x86_64-dragonfly5.5/expr_transform.o a - /construction/math/cvc3/cvc3-2.4.1/obj/theory_core/x86_64-dragonfly5.5/bryant.o gmake[3]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/theory_core' cd theory_arith && gmake gmake[3]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/theory_arith' Making dependencies for arith_theorem_producer_old.cpp arith_theorem_producer.cpp arith_theorem_producer3.cpp theory_arith.cpp theory_arith_old.cpp theory_arith_new.cpp theory_arith3.cpp g++ -M -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/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 >> /construction/math/cvc3/cvc3-2.4.1/obj/theory_arith/x86_64-dragonfly5.5/Makefile.tmp g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c arith_theorem_producer3.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/theory_arith/x86_64-dragonfly5.5/arith_theorem_producer3.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c arith_theorem_producer.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/theory_arith/x86_64-dragonfly5.5/arith_theorem_producer.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c arith_theorem_producer_old.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/theory_arith/x86_64-dragonfly5.5/arith_theorem_producer_old.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c theory_arith.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/theory_arith/x86_64-dragonfly5.5/theory_arith.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c theory_arith_old.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/theory_arith/x86_64-dragonfly5.5/theory_arith_old.o' arith_theorem_producer_old.cpp: In member function 'virtual CVC3::Theorem CVC3::ArithTheoremProducerOld::canonMult(const CVC3::Expr&)': arith_theorem_producer_old.cpp:797:50: warning: logical not is only applied to the left hand side of comparison [-Wlogical-not-parentheses] if (count_non_trivial > 0 && !count_constants == (e.arity() - 1)) { ^~ arith_theorem_producer_old.cpp:797:33: note: add parentheses around left hand side expression to silence this warning if (count_non_trivial > 0 && !count_constants == (e.arity() - 1)) { ^~~~~~~~~~~~~~~~ ( ) theory_arith_old.cpp: In member function 'bool CVC3::TheoryArithOld::findBounds(const CVC3::Expr&, CVC3::Rational&, CVC3::Rational&)': theory_arith_old.cpp:2782:24: warning: variable 'strictUB' set but not used [-Wunused-but-set-variable] bool strictLB=false, strictUB=false; ^~~~~~~~ g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c theory_arith_new.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/theory_arith/x86_64-dragonfly5.5/theory_arith_new.o' theory_arith_new.cpp: In member function 'bool CVC3::TheoryArithNew::findBounds(const CVC3::Expr&, CVC3::Rational&, CVC3::Rational&)': theory_arith_new.cpp:1350:24: warning: variable 'strictUB' set but not used [-Wunused-but-set-variable] bool strictLB=false, strictUB=false; ^~~~~~~~ theory_arith_new.cpp: In member function 'std::__cxx11::string CVC3::TheoryArithNew::tableauxAsString() const': theory_arith_new.cpp:3350:30: warning: variable 'row_end' set but not used [-Wunused-but-set-variable] TebleauxMap::const_iterator row_end = tableaux.end(); ^~~~~~~ g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c theory_arith3.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/theory_arith/x86_64-dragonfly5.5/theory_arith3.o' theory_arith3.cpp: In member function 'bool CVC3::TheoryArith3::findBounds(const CVC3::Expr&, CVC3::Rational&, CVC3::Rational&)': theory_arith3.cpp:2199:24: warning: variable 'strictUB' set but not used [-Wunused-but-set-variable] bool strictLB=false, strictUB=false; ^~~~~~~~ ar ruvs '/construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libtheory_arith.a' /construction/math/cvc3/cvc3-2.4.1/obj/theory_arith/x86_64-dragonfly5.5/arith_theorem_producer_old.o /construction/math/cvc3/cvc3-2.4.1/obj/theory_arith/x86_64-dragonfly5.5/arith_theorem_producer.o /construction/math/cvc3/cvc3-2.4.1/obj/theory_arith/x86_64-dragonfly5.5/arith_theorem_producer3.o /construction/math/cvc3/cvc3-2.4.1/obj/theory_arith/x86_64-dragonfly5.5/theory_arith.o /construction/math/cvc3/cvc3-2.4.1/obj/theory_arith/x86_64-dragonfly5.5/theory_arith_old.o /construction/math/cvc3/cvc3-2.4.1/obj/theory_arith/x86_64-dragonfly5.5/theory_arith_new.o /construction/math/cvc3/cvc3-2.4.1/obj/theory_arith/x86_64-dragonfly5.5/theory_arith3.o /usr/libexec/binutils227/elf/ar: `u' modifier ignored since `D' is the default (see `U') /usr/libexec/binutils227/elf/ar: creating /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libtheory_arith.a a - /construction/math/cvc3/cvc3-2.4.1/obj/theory_arith/x86_64-dragonfly5.5/arith_theorem_producer_old.o a - /construction/math/cvc3/cvc3-2.4.1/obj/theory_arith/x86_64-dragonfly5.5/arith_theorem_producer.o a - /construction/math/cvc3/cvc3-2.4.1/obj/theory_arith/x86_64-dragonfly5.5/arith_theorem_producer3.o a - /construction/math/cvc3/cvc3-2.4.1/obj/theory_arith/x86_64-dragonfly5.5/theory_arith.o a - /construction/math/cvc3/cvc3-2.4.1/obj/theory_arith/x86_64-dragonfly5.5/theory_arith_old.o a - /construction/math/cvc3/cvc3-2.4.1/obj/theory_arith/x86_64-dragonfly5.5/theory_arith_new.o a - /construction/math/cvc3/cvc3-2.4.1/obj/theory_arith/x86_64-dragonfly5.5/theory_arith3.o gmake[3]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/theory_arith' cd theory_array && gmake gmake[3]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/theory_array' Making dependencies for array_theorem_producer.cpp theory_array.cpp g++ -M -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include array_theorem_producer.cpp theory_array.cpp >> /construction/math/cvc3/cvc3-2.4.1/obj/theory_array/x86_64-dragonfly5.5/Makefile.tmp g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c array_theorem_producer.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/theory_array/x86_64-dragonfly5.5/array_theorem_producer.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c theory_array.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/theory_array/x86_64-dragonfly5.5/theory_array.o' ar ruvs '/construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libtheory_array.a' /construction/math/cvc3/cvc3-2.4.1/obj/theory_array/x86_64-dragonfly5.5/array_theorem_producer.o /construction/math/cvc3/cvc3-2.4.1/obj/theory_array/x86_64-dragonfly5.5/theory_array.o /usr/libexec/binutils227/elf/ar: `u' modifier ignored since `D' is the default (see `U') /usr/libexec/binutils227/elf/ar: creating /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libtheory_array.a a - /construction/math/cvc3/cvc3-2.4.1/obj/theory_array/x86_64-dragonfly5.5/array_theorem_producer.o a - /construction/math/cvc3/cvc3-2.4.1/obj/theory_array/x86_64-dragonfly5.5/theory_array.o gmake[3]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/theory_array' cd theory_bitvector && gmake gmake[3]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/theory_bitvector' Making dependencies for bitvector_theorem_producer.cpp theory_bitvector.cpp g++ -M -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include bitvector_theorem_producer.cpp theory_bitvector.cpp >> /construction/math/cvc3/cvc3-2.4.1/obj/theory_bitvector/x86_64-dragonfly5.5/Makefile.tmp g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c bitvector_theorem_producer.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/theory_bitvector/x86_64-dragonfly5.5/bitvector_theorem_producer.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c theory_bitvector.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/theory_bitvector/x86_64-dragonfly5.5/theory_bitvector.o' theory_bitvector.cpp: In member function 'CVC3::Theorem CVC3::TheoryBitvector::rewriteBV(const CVC3::Expr&, CVC3::ExprMap&, int)': theory_bitvector.cpp:1063:11: warning: variable 'hi' set but not used [-Wunused-but-set-variable] int hi(-1), low(-1); ^~ bitvector_theorem_producer.cpp: In member function 'virtual CVC3::Theorem CVC3::BitvectorTheoremProducer::bitwiseFlatten(const CVC3::Expr&, int)': bitvector_theorem_producer.cpp:2996:26: warning: variable 'jend' set but not used [-Wunused-but-set-variable] vector::iterator jend = flattenkids.end(); ^~~~ ar ruvs '/construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libtheory_bitvector.a' /construction/math/cvc3/cvc3-2.4.1/obj/theory_bitvector/x86_64-dragonfly5.5/bitvector_theorem_producer.o /construction/math/cvc3/cvc3-2.4.1/obj/theory_bitvector/x86_64-dragonfly5.5/theory_bitvector.o /usr/libexec/binutils227/elf/ar: `u' modifier ignored since `D' is the default (see `U') /usr/libexec/binutils227/elf/ar: creating /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libtheory_bitvector.a a - /construction/math/cvc3/cvc3-2.4.1/obj/theory_bitvector/x86_64-dragonfly5.5/bitvector_theorem_producer.o a - /construction/math/cvc3/cvc3-2.4.1/obj/theory_bitvector/x86_64-dragonfly5.5/theory_bitvector.o gmake[3]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/theory_bitvector' cd theory_datatype && gmake gmake[3]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/theory_datatype' Making dependencies for datatype_theorem_producer.cpp theory_datatype.cpp theory_datatype_lazy.cpp g++ -M -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include datatype_theorem_producer.cpp theory_datatype.cpp theory_datatype_lazy.cpp >> /construction/math/cvc3/cvc3-2.4.1/obj/theory_datatype/x86_64-dragonfly5.5/Makefile.tmp g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c datatype_theorem_producer.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/theory_datatype/x86_64-dragonfly5.5/datatype_theorem_producer.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c theory_datatype.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/theory_datatype/x86_64-dragonfly5.5/theory_datatype.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c theory_datatype_lazy.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/theory_datatype/x86_64-dragonfly5.5/theory_datatype_lazy.o' ar ruvs '/construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libtheory_datatype.a' /construction/math/cvc3/cvc3-2.4.1/obj/theory_datatype/x86_64-dragonfly5.5/datatype_theorem_producer.o /construction/math/cvc3/cvc3-2.4.1/obj/theory_datatype/x86_64-dragonfly5.5/theory_datatype.o /construction/math/cvc3/cvc3-2.4.1/obj/theory_datatype/x86_64-dragonfly5.5/theory_datatype_lazy.o /usr/libexec/binutils227/elf/ar: `u' modifier ignored since `D' is the default (see `U') /usr/libexec/binutils227/elf/ar: creating /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libtheory_datatype.a a - /construction/math/cvc3/cvc3-2.4.1/obj/theory_datatype/x86_64-dragonfly5.5/datatype_theorem_producer.o a - /construction/math/cvc3/cvc3-2.4.1/obj/theory_datatype/x86_64-dragonfly5.5/theory_datatype.o a - /construction/math/cvc3/cvc3-2.4.1/obj/theory_datatype/x86_64-dragonfly5.5/theory_datatype_lazy.o gmake[3]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/theory_datatype' cd theory_quant && gmake gmake[3]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/theory_quant' Making dependencies for theory_quant.cpp quant_theorem_producer.cpp g++ -M -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include theory_quant.cpp quant_theorem_producer.cpp >> /construction/math/cvc3/cvc3-2.4.1/obj/theory_quant/x86_64-dragonfly5.5/Makefile.tmp g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c theory_quant.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/theory_quant/x86_64-dragonfly5.5/theory_quant.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c quant_theorem_producer.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/theory_quant/x86_64-dragonfly5.5/quant_theorem_producer.o' theory_quant.cpp: In member function 'virtual CVC3::Expr CVC3::TheoryQuant::parseExprOp(const CVC3::Expr&)': theory_quant.cpp:9077:21: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] catch (Exception e){ ^ ar ruvs '/construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libtheory_quant.a' /construction/math/cvc3/cvc3-2.4.1/obj/theory_quant/x86_64-dragonfly5.5/theory_quant.o /construction/math/cvc3/cvc3-2.4.1/obj/theory_quant/x86_64-dragonfly5.5/quant_theorem_producer.o /usr/libexec/binutils227/elf/ar: `u' modifier ignored since `D' is the default (see `U') /usr/libexec/binutils227/elf/ar: creating /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libtheory_quant.a a - /construction/math/cvc3/cvc3-2.4.1/obj/theory_quant/x86_64-dragonfly5.5/theory_quant.o a - /construction/math/cvc3/cvc3-2.4.1/obj/theory_quant/x86_64-dragonfly5.5/quant_theorem_producer.o gmake[3]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/theory_quant' cd theory_records && gmake gmake[3]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/theory_records' Making dependencies for theory_records.cpp records_theorem_producer.cpp g++ -M -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include theory_records.cpp records_theorem_producer.cpp >> /construction/math/cvc3/cvc3-2.4.1/obj/theory_records/x86_64-dragonfly5.5/Makefile.tmp g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c theory_records.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/theory_records/x86_64-dragonfly5.5/theory_records.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c records_theorem_producer.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/theory_records/x86_64-dragonfly5.5/records_theorem_producer.o' ar ruvs '/construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libtheory_records.a' /construction/math/cvc3/cvc3-2.4.1/obj/theory_records/x86_64-dragonfly5.5/theory_records.o /construction/math/cvc3/cvc3-2.4.1/obj/theory_records/x86_64-dragonfly5.5/records_theorem_producer.o /usr/libexec/binutils227/elf/ar: `u' modifier ignored since `D' is the default (see `U') /usr/libexec/binutils227/elf/ar: creating /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libtheory_records.a a - /construction/math/cvc3/cvc3-2.4.1/obj/theory_records/x86_64-dragonfly5.5/theory_records.o a - /construction/math/cvc3/cvc3-2.4.1/obj/theory_records/x86_64-dragonfly5.5/records_theorem_producer.o gmake[3]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/theory_records' cd theory_simulate && gmake gmake[3]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/theory_simulate' Making dependencies for theory_simulate.cpp simulate_theorem_producer.cpp g++ -M -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include theory_simulate.cpp simulate_theorem_producer.cpp >> /construction/math/cvc3/cvc3-2.4.1/obj/theory_simulate/x86_64-dragonfly5.5/Makefile.tmp g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c theory_simulate.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/theory_simulate/x86_64-dragonfly5.5/theory_simulate.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c simulate_theorem_producer.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/theory_simulate/x86_64-dragonfly5.5/simulate_theorem_producer.o' ar ruvs '/construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libtheory_simulate.a' /construction/math/cvc3/cvc3-2.4.1/obj/theory_simulate/x86_64-dragonfly5.5/theory_simulate.o /construction/math/cvc3/cvc3-2.4.1/obj/theory_simulate/x86_64-dragonfly5.5/simulate_theorem_producer.o /usr/libexec/binutils227/elf/ar: `u' modifier ignored since `D' is the default (see `U') /usr/libexec/binutils227/elf/ar: creating /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libtheory_simulate.a a - /construction/math/cvc3/cvc3-2.4.1/obj/theory_simulate/x86_64-dragonfly5.5/theory_simulate.o a - /construction/math/cvc3/cvc3-2.4.1/obj/theory_simulate/x86_64-dragonfly5.5/simulate_theorem_producer.o gmake[3]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/theory_simulate' cd theory_uf && gmake gmake[3]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/theory_uf' Making dependencies for uf_theorem_producer.cpp theory_uf.cpp g++ -M -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include uf_theorem_producer.cpp theory_uf.cpp >> /construction/math/cvc3/cvc3-2.4.1/obj/theory_uf/x86_64-dragonfly5.5/Makefile.tmp g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c uf_theorem_producer.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/theory_uf/x86_64-dragonfly5.5/uf_theorem_producer.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c theory_uf.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/theory_uf/x86_64-dragonfly5.5/theory_uf.o' ar ruvs '/construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libtheory_uf.a' /construction/math/cvc3/cvc3-2.4.1/obj/theory_uf/x86_64-dragonfly5.5/uf_theorem_producer.o /construction/math/cvc3/cvc3-2.4.1/obj/theory_uf/x86_64-dragonfly5.5/theory_uf.o /usr/libexec/binutils227/elf/ar: `u' modifier ignored since `D' is the default (see `U') /usr/libexec/binutils227/elf/ar: creating /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libtheory_uf.a a - /construction/math/cvc3/cvc3-2.4.1/obj/theory_uf/x86_64-dragonfly5.5/uf_theorem_producer.o a - /construction/math/cvc3/cvc3-2.4.1/obj/theory_uf/x86_64-dragonfly5.5/theory_uf.o gmake[3]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/theory_uf' cd search && gmake gmake[3]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/search' Making dependencies for clause.cpp search_impl_base.cpp search.cpp search_fast.cpp search_theorem_producer.cpp search_sat.cpp search_simple.cpp variable.cpp circuit.cpp decision_engine.cpp decision_engine_dfs.cpp LFSCObject.cpp LFSCUtilProof.cpp LFSCBoolProof.cpp LFSCConvert.cpp LFSCLraProof.cpp LFSCPrinter.cpp LFSCProof.cpp TReturn.cpp Util.cpp g++ -M -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DDPLL_BASIC -I/usr/local/include clause.cpp search_impl_base.cpp search.cpp search_fast.cpp search_theorem_producer.cpp search_sat.cpp search_simple.cpp variable.cpp circuit.cpp decision_engine.cpp decision_engine_dfs.cpp LFSCObject.cpp LFSCUtilProof.cpp LFSCBoolProof.cpp LFSCConvert.cpp LFSCLraProof.cpp LFSCPrinter.cpp LFSCProof.cpp TReturn.cpp Util.cpp >> /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/Makefile.tmp g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DDPLL_BASIC -I/usr/local/include -c clause.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/clause.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DDPLL_BASIC -I/usr/local/include -c search_fast.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/search_fast.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DDPLL_BASIC -I/usr/local/include -c search.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/search.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DDPLL_BASIC -I/usr/local/include -c search_impl_base.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/search_impl_base.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DDPLL_BASIC -I/usr/local/include -c search_theorem_producer.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/search_theorem_producer.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DDPLL_BASIC -I/usr/local/include -c search_sat.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/search_sat.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DDPLL_BASIC -I/usr/local/include -c search_simple.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/search_simple.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DDPLL_BASIC -I/usr/local/include -c variable.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/variable.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DDPLL_BASIC -I/usr/local/include -c circuit.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/circuit.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DDPLL_BASIC -I/usr/local/include -c decision_engine.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/decision_engine.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DDPLL_BASIC -I/usr/local/include -c decision_engine_dfs.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/decision_engine_dfs.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DDPLL_BASIC -I/usr/local/include -c LFSCObject.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/LFSCObject.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DDPLL_BASIC -I/usr/local/include -c LFSCUtilProof.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/LFSCUtilProof.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DDPLL_BASIC -I/usr/local/include -c LFSCBoolProof.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/LFSCBoolProof.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DDPLL_BASIC -I/usr/local/include -c LFSCConvert.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/LFSCConvert.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DDPLL_BASIC -I/usr/local/include -c LFSCLraProof.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/LFSCLraProof.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DDPLL_BASIC -I/usr/local/include -c LFSCPrinter.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/LFSCPrinter.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DDPLL_BASIC -I/usr/local/include -c LFSCProof.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/LFSCProof.o' LFSCProof.cpp: In member function 'virtual int LFSCProof::checkOp()': LFSCProof.cpp:91:11: warning: unused variable 'o' [-Wunused-variable] int o = getChild( a )->checkOp(); ^ LFSCProof.cpp: In static member function 'static LFSCProof* LFSCProof::Make_CNF(const CVC3::Expr&, const CVC3::Expr&, int)': LFSCProof.cpp:193:11: warning: unused variable 'm2' [-Wunused-variable] int m2 = queryM( ec[1] ); ^~ g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DDPLL_BASIC -I/usr/local/include -c TReturn.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/TReturn.o' TReturn.cpp: In static member function 'static int TReturn::normalize_tr(const CVC3::Expr&, TReturn*&, int, bool, bool)': TReturn.cpp:127:12: warning: unused variable 'torig' [-Wunused-variable] TReturn* torig = t1; ^~~~~ g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DDPLL_BASIC -I/usr/local/include -c Util.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/Util.o' ar ruvs '/construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libsearch.a' /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/clause.o /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/search_impl_base.o /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/search.o /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/search_fast.o /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/search_theorem_producer.o /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/search_sat.o /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/search_simple.o /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/variable.o /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/circuit.o /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/decision_engine.o /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/decision_engine_dfs.o /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/LFSCObject.o /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/LFSCUtilProof.o /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/LFSCBoolProof.o /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/LFSCConvert.o /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/LFSCLraProof.o /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/LFSCPrinter.o /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/LFSCProof.o /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/TReturn.o /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/Util.o /usr/libexec/binutils227/elf/ar: `u' modifier ignored since `D' is the default (see `U') /usr/libexec/binutils227/elf/ar: creating /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libsearch.a a - /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/clause.o a - /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/search_impl_base.o a - /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/search.o a - /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/search_fast.o a - /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/search_theorem_producer.o a - /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/search_sat.o a - /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/search_simple.o a - /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/variable.o a - /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/circuit.o a - /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/decision_engine.o a - /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/decision_engine_dfs.o a - /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/LFSCObject.o a - /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/LFSCUtilProof.o a - /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/LFSCBoolProof.o a - /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/LFSCConvert.o a - /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/LFSCLraProof.o a - /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/LFSCPrinter.o a - /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/LFSCProof.o a - /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/TReturn.o a - /construction/math/cvc3/cvc3-2.4.1/obj/search/x86_64-dragonfly5.5/Util.o gmake[3]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/search' cd parser && gmake gmake[3]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/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 bison -d -y -o parsesmtlib2.cpp -p smtlib2 --debug -v smtlib2.y Lisp.y:75.33-36: warning: POSIX Yacc does not support string literals [-Wyacc] %token BINARY_TOK "0b" ^~~~ Lisp.y:76.33-36: warning: POSIX Yacc does not support string literals [-Wyacc] %token HEX_TOK "0x" PL.y:192.25 -34: ^~~~ warning: POSIX Yacc does not support string literals [-Wyacc] %token DISTINCT_TOK "DISTINCT" ^~~~~~~~~~ PL.y:193.33-37: warning: POSIX Yacc does not support string literals [-Wyacc] %token AND_TOK "AND" ^~~~~ PL.y:194.33-39: warning: POSIX Yacc does not support string literals [-Wyacc] %token ARRAY_TOK "ARRAY" ^~~~~~~ PL.y:195.33-41: warning: POSIX Yacc does not support string literals [-Wyacc] %token BOOLEAN_TOK "BOOLEAN" ^~~~~~~~~ PL.y:196.33-42: warning: POSIX Yacc does not support string literals [-Wyacc] %token DATATYPE_TOK "DATATYPE" ^~~~~~~~~~ PL.y:197.33-38: warning: POSIX Yacc does not support string literals [-Wyacc] %token ELSE_TOK "ELSE" ^~~~~~ PL.y:198.33-39: warning: POSIX Yacc does not support string literals [-Wyacc] %token ELSIF_TOK "ELSIF" ^~~~~~~ PL.y:199.33-37: warning: POSIX Yacc does not support string literals [-Wyacc] %token END_TOK "END" ^~~~~ PL.y:200.33-39: warning: POSIX Yacc does not support string literals [-Wyacc] %token ENDIF_TOK "ENDIF" ^~~~~~~ PL.y:201.33-40: warning: POSIX Yacc does not support string literals [-Wyacc] %token EXISTS_TOK "EXISTS" ^~~~~~~~ PL.y:202.33-39: warning: POSIX Yacc does not support string literals [-Wyacc] %token FALSELIT_TOK "FALSE" ^~~~~~~ PL.y:203.33-40: warning: POSIX Yacc does not support string literals [-Wyacc] %token FORALL_TOK "FORALL" ^~~~~~~~ PL.y:204.33-36: warning: POSIX Yacc does not support string literals [-Wyacc] %token IN_TOK "IN" ^~~~ PL.y:205.33-36: warning: POSIX Yacc does not support string literals [-Wyacc] %token IF_TOK "IF" ^~~~ PL.y:206.33-40: warning: POSIX Yacc does not support string literals [-Wyacc] %token LAMBDA_TOK "LAMBDA" ^~~~~~~~ PL.y:207.33-42: warning: POSIX Yacc does not support string literals [-Wyacc] %token SIMULATE_TOK "SIMULATE" ^~~~~~~~~~ PL.y:208.33-37: warning: POSIX Yacc does not support string literals [-Wyacc] %token LET_TOK "LET" ^~~~~ PL.y:209.33-37: warning: POSIX Yacc does not support string literals [-Wyacc] %token NOT_TOK "NOT" ^~~~~ PL.y:210.33-44: warning: POSIX Yacc does not support string literals [-Wyacc] %token IS_INTEGER_TOK "IS_INTEGER" ^~~~~~~~~~~~ PL.y:211.33-36: warning: POSIX Yacc does not support string literals [-Wyacc] %token OF_TOK "OF" ^~~~ PL.y:212.33-36: warning: POSIX Yacc does not support string literals [-Wyacc] %token OR_TOK "OR" ^~~~ PL.y:213.33-38: warning: POSIX Yacc does not support string literals [-Wyacc] %token REAL_TOK "REAL" ^~~~~~ PL.y:214.33-37: warning: POSIX Yacc does not support string literals [-Wyacc] %token INT_TOK "INT" ^~~~~ PL.y:215.33-41: warning: POSIX Yacc does not support string literals [-Wyacc] %token SUBTYPE_TOK "SUBTYPE" ^~~~~~~~~ PL.y:216.33-43: warning: POSIX Yacc does not support string literals [-Wyacc] %token BITVECTOR_TOK "BITVECTOR" ^~~~~~~~~~~ PL.y:217.33-38: warning: POSIX Yacc does not support string literals [-Wyacc] %token THEN_TOK "THEN" ^~~~~~ PL.y:218.33-38: warning: POSIX Yacc does not support string literals [-Wyacc] %token TRUELIT_TOK "TRUE" ^~~~~~ PL.y:219.33-38: warning: POSIX Yacc does not support string literals [-Wyacc] %token TYPE_TOK "TYPE" ^~~~~~ PL.y:220.33-38: warning: POSIX Yacc does not support string literals [-Wyacc] %token WITH_TOK "WITH" ^~~~~~ PL.y:221.33-37: warning: POSIX Yacc does not support string literals [-Wyacc] %token XOR_TOK "XOR" ^~~~~ PL.y:222.33-37: warning: POSIX Yacc does not support string literals [-Wyacc] %token TCC_TOK "TCC" ^~~~~ PL.y:223.33-41: warning: POSIX Yacc does not support string literals [-Wyacc] %token PATTERN_TOK "PATTERN" ^~~~~~~~~ PL.y:227.33-36: warning: POSIX Yacc does not support string literals [-Wyacc] %token DOTDOT_TOK ".." ^~~~ PL.y:228.33-36: warning: POSIX Yacc does not support string literals [-Wyacc] %token ASSIGN_TOK ":=" ^~~~ PL.y:229.33-36: warning: POSIX Yacc does not support string literals [-Wyacc] %token NEQ_TOK "/=" ^~~~ PL.y:230.33-36: warning: POSIX Yacc does not support string literals [-Wyacc] %token IMPLIES_TOK "=>" ^~~~ PL.y:231.33-37: warning: POSIX Yacc does not support string literals [-Wyacc] %token IFF_TOK "<=>" ^~~~~ PL.y:232.33-35: warning: POSIX Yacc does not support string literals [-Wyacc] %token PLUS_TOK "+" ^~~ PL.y:233.33-35: warning: POSIX Yacc does not support string literals [-Wyacc] %token MINUS_TOK "-" ^~~ PL.y:234.33-35: warning: POSIX Yacc does not support string literals [-Wyacc] %token MULT_TOK "*" ^~~ PL.y:235.33-35: warning: POSIX Yacc does not support string literals [-Wyacc] %token POW_TOK "^" ^~~ PL.y:236.33-35: warning: POSIX Yacc does not support string literals [-Wyacc] %token DIV_TOK "/" ^~~ PL.y:237.33-37: warning: POSIX Yacc does not support string literals [-Wyacc] %token MOD_TOK "MOD" ^~~~~ PL.y:238.33-37: warning: POSIX Yacc does not support string literals [-Wyacc] %token INTDIV_TOK "DIV" ^~~~~ PL.y:239.33-35: warning: POSIX Yacc does not support string literals [-Wyacc] %token LT_TOK "<" ^~~ PL.y:240.33-36: warning: POSIX Yacc does not support string literals [-Wyacc] %token LE_TOK "<=" ^~~~ PL.y:241.33-35: warning: POSIX Yacc does not support string literals [-Wyacc] %token GT_TOK ">" ^~~ PL.y:242.33-36: warning: POSIX Yacc does not support string literals [-Wyacc] %token GE_TOK ">=" ^~~~ PL.y:243.33-39: warning: POSIX Yacc does not support string literals [-Wyacc] %token FLOOR_TOK "FLOOR" ^~~~~~~ PL.y:244.34-37: warning: POSIX Yacc does not support string literals [-Wyacc] %token LEFTSHIFT_TOK "<<" ^~~~ PL.y:245.34-37: warning: POSIX Yacc does not support string literals [-Wyacc] %token RIGHTSHIFT_TOK ">>" ^~~~ PL.y:246.33-40: warning: POSIX Yacc does not support string literals [-Wyacc] %token BVPLUS_TOK "BVPLUS" ^~~~~~~~ PL.y:247.33-39: warning: POSIX Yacc does not support string literals [-Wyacc] %token BVSUB_TOK "BVSUB" ^~~~~~~ PL.y:248.33-40: warning: POSIX Yacc does not support string literals [-Wyacc] %token BVUDIV_TOK "BVUDIV" ^~~~~~~~ PL.y:249.33-40: warning: POSIX Yacc does not support string literals [-Wyacc] %token BVSDIV_TOK "BVSDIV" ^~~~~~~~ PL.y:250.33-40: warning: POSIX Yacc does not support string literals [-Wyacc] %token BVUREM_TOK "BVUREM" ^~~~~~~~ PL.y:251.33-40: warning: POSIX Yacc does not support string literals [-Wyacc] %token BVSREM_TOK "BVSREM" ^~~~~~~~ PL.y:252.33-40: warning: POSIX Yacc does not support string literals [-Wyacc] %token BVSMOD_TOK "BVSMOD" ^~~~~~~~ PL.y:253.33-39: warning: POSIX Yacc does not support string literals [-Wyacc] %token BVSHL_TOK "BVSHL" ^~~~~~~ PL.y:254.33-40: warning: POSIX Yacc does not support string literals [-Wyacc] %token BVASHR_TOK "BVASHR" ^~~~~~~~ PL.y:255.33-40: warning: POSIX Yacc does not support string literals [-Wyacc] %token BVLSHR_TOK "BVLSHR" ^~~~~~~~ PL.y:256.33-42: warning: POSIX Yacc does not support string literals [-Wyacc] %token BVUsmtlib2.y: Mwarning: I4 shift/reduce conflictsNUS [-Wconflicts-sr]_TOK "BVUMINUS" ^~~~~~~~~~ PL.y:257.33-40: warning: POSIX Yacc does not support string literals [-Wyacc] %token BVMULT_TOK "BVMULT" ^~~~~~~~ PL.y:258.33-36: warning: POSIX Yacc does not support string literals [-Wyacc] %token SQHASH_TOK "[#" ^~~~ PL.y:259.33-36: warning: POSIX Yacc does not support string literals [-Wyacc] %token HASHSQ_TOK "#]" ^~~~ PL.y:260.33-36: warning: POSIX Yacc does not support string literals [-Wyacc] %token PARENHASH_TOK "(#" ^~~~ PL.y:261.33-36: warning: POSIX Yacc does not support string literals [-Wyacc] %token HASHPAREN_TOK "#)" ^~~~ PL.y:262.33-36: warning: POSIX Yacc does not support string literals [-Wyacc] %token ARROW_TOK "->" ^~~~ PL.y:263.33-35: warning: POSIX Yacc does not support string literals [-Wyacc] %token BVNEG_TOK "~" ^~~ PL.y:264.33-35: warning: POSIX Yacc does not support string literals [-Wyacc] %token BVAND_TOK "&" ^~~ PL.y:265.33-35: warning: POSIX Yacc does not support string literals [-Wyacc] %token MID_TOK "|" ^~~ PL.y:266.33-39: warning: POSIX Yacc does not support string literals [-Wyacc] %token BVXOR_TOK "BVXOR" ^~~~~~~ PL.y:267.33-40: warning: POSIX Yacc does not support string literals [-Wyacc] %token BVNAND_TOK "BVNAND" ^~~~~~~~ PL.y:268.33-39: warning: POSIX Yacc does not support string literals [-Wyacc] %token BVNOR_TOK "BVNOR" ^~~~~~~ PL.y:269.33-40: warning: POSIX Yacc does not support string literals [-Wyacc] %token BVCOMP_TOK "BVCOMP" ^~~~~~~~ PL.y:270.33-40: warning: POSIX Yacc does not support string literals [-Wyacc] %token BVXNOR_TOK "BVXNOR" ^~~~~~~~ PL.y:271.33-35: warning: POSIX Yacc does not support string literals [-Wyacc] %token CONCAT_TOK "@" ^~~ PL.y:272.33-41: warning: POSIX Yacc does not support string literals [-Wyacc] %token BVTOINT_TOK "BVTOINT" ^~~~~~~~~ PL.y:273.33-41: warning: POSIX Yacc does not support string literals [-Wyacc] %token INTTOBV_TOK "INTTOBV" ^~~~~~~~~ PL.y:274.33-45: warning: POSIX Yacc does not support string literals [-Wyacc] %token BOOLEXTRACT_TOK "BOOLEXTRACT" ^~~~~~~~~~~~~ PL.y:275.33-38: warning: POSIX Yacc does not support string literals [-Wyacc] %token BVLT_TOK "BVLT" ^~~~~~ PL.y:276.33-38: warning: POSIX Yacc does not support string literals [-Wyacc] %token BVGT_TOK "BVGT" ^~~~~~ PL.y:277.33-38: warning: POSIX Yacc does not support string literals [-Wyacc] %token BVLE_TOK "BVLE" ^~~~~~ PL.y:278.33-38: warning: POSIX Yacc does not support string literals [-Wyacc] %token BVGE_TOK "BVGE" ^~~~~~ PL.y:279.33-36: warning: POSIX Yacc does not support string literals [-Wyacc] %token SX_TOK "SX" ^~~~ PL.y:280.33-46: warning: POSIX Yacc does not support string literals [-Wyacc] %token BVZEROEXTEND_TOK "BVZEROEXTEND" ^~~~~~~~~~~~~~ PL.y:281.33-42: warning: POSIX Yacc does not support string literals [-Wyacc] %token BVREPEAT_TOK "BVREPEAT" ^~~~~~~~~~ PL.y:282.33-40: warning: POSIX Yacc does not support string literals [-Wyacc] %token BVROTL_TOK "BVROTL" ^~~~~~~~ PL.y:283.33-40: warning: POSIX Yacc does not support string literals [-Wyacc] %token BVROTR_TOK "BVROTR" ^~~~~~~~ PL.y:284.33-39: warning: POSIX Yacc does not support string literals [-Wyacc] %token BVSLT_TOK "BVSLT" ^~~~~~~ PL.y:285.33-39: warning: POSIX Yacc does not support string literals [-Wyacc] %token BVSGT_TOK "BVSGT" ^~~~~~~ PL.y:286.33-39: warning: POSIX Yacc does not support string literals [-Wyacc] %token BVSLE_TOK "BVSLE" ^~~~~~~ PL.y:287.33-39: warning: POSIX Yacc does not support string literals [-Wyacc] %token BVSGE_TOK "BVSGE" ^~~~~~~ PL.y:291.33-49: warning: POSIX Yacc does not support string literals [-Wyacc] %token ARITH_VAR_ORDER_TOK "ARITH_VAR_ORDER" ^~~~~~~~~~~~~~~~~ PL.y:292.33-40: warning: POSIX Yacc does not support string literals [-Wyacc] %token ASSERT_TOK "ASSERT" ^~~~~~~~ PL.y:293.33-39: warning: POSIX Yacc does not support string literals [-Wyacc] %token QUERY_TOK "QUERY" ^~~~~~~ PL.y:294.33-42: warning: POSIX Yacc does not support string literals [-Wyacc] %token CHECKSAT_TOK "CHECKSAT" ^~~~~~~~~~ PL.y:295.33-42: warning: POSIX Yacc does not support string literals [-Wyacc] %token CONTINUE_TOK "CONTINUE" ^~~~~~~~~~ PL.y:296.33-41: warning: POSIX Yacc does not support string literals [-Wyacc] %token RESTART_TOK "RESTART" ^~~~~~~~~ PL.y:297.33-38: warning: POSIX Yacc does not support string literals [-Wyacc] %token HELP_TOK "HELP" ^~~~~~ PL.y:298.33-37: warning: POSIX Yacc does not support string literals [-Wyacc] %token DBG_TOK "DBG" ^~~~~ PL.y:299.33-39: warning: POSIX Yacc does not support string literals [-Wyacc] %token TRACE_TOK "TRACE" ^~~~~~~ PL.y:300.33-41: warning: POSIX Yacc does not support string literals [-Wyacc] %token UNTRACE_TOK "UNTRACE" ^~~~~~~~~ PL.y:301.33-40: warning: POSIX Yacc does not support string literals [-Wyacc] %token OPTION_TOK "OPTION" ^~~~~~~~ PL.y:302.33-43: warning: POSIX Yacc does not support string literals [-Wyacc] %token TRANSFORM_TOK "TRANSFORM" ^~~~~~~~~~~ PL.y:303.33-39: warning: POSIX Yacc does not support string literals [-Wyacc] %token PRINT_TOK "PRINT" ^~~~~~~ PL.y:304.33-44: warning: POSIX Yacc does not support string literals [-Wyacc] %token PRINT_TYPE_TOK "PRINT_TYPE" ^~~~~~~~~~~~ PL.y:305.33-38: warning: POSIX Yacc does not support string literals [-Wyacc] %token CALL_TOK "CALL" ^~~~~~ PL.y:306.33-38: warning: POSIX Yacc does not support string literals [-Wyacc] %token ECHO_TOK "ECHO" ^~~~~~ PL.y:307.33-41: warning: POSIX Yacc does not support string literals [-Wyacc] %token INCLUDE_TOK "INCLUDE" ^~~~~~~~~ PL.y:308.33-44: warning: POSIX Yacc does not support string literals [-Wyacc] %token DUMP_PROOF_TOK "DUMP_PROOF" ^~~~~~~~~~~~ PL.y:309.33-50: warning: POSIX Yacc does not support string literals [-Wyacc] %token DUMP_ASSUMPTIONS_TOK "DUMP_ASSUMPTIONS" ^~~~~~~~~~~~~~~~~~ PL.y:310.33-42: warning: POSIX Yacc does not support string literals [-Wyacc] %token DUMP_SIG_TOK "DUMP_SIG" ^~~~~~~~~~ PL.y:311.33-42: warning: POSIX Yacc does not support string literals [-Wyacc] %token DUMP_TCC_TOK "DUMP_TCC" ^~~~~~~~~~ PL.y:312.34-55: warning: POSIX Yacc does not support string literals [-Wyacc] %token DUMP_TCC_ASSUMPTIONS_TOK "DUMP_TCC_ASSUMPTIONS" ^~~~~~~~~~~~~~~~~~~~~~ PL.y:313.33-48: warning: POSIX Yacc does not support string literals [-Wyacc] %token DUMP_TCC_PROOF_TOK "DUMP_TCC_PROOF" ^~~~~~~~~~~~~~~~ PL.y:314.33-46: warning: POSIX Yacc does not support string literals [-Wyacc] %token DUMP_CLOSURE_TOK "DUMP_CLOSURE" ^~~~~~~~~~~~~~ PL.y:315.33-52: warning: POSIX Yacc does not support string literals [-Wyacc] %token DUMP_CLOSURE_PROOF_TOK "DUMP_CLOSURE_PROOF" ^~~~~~~~~~~~~~~~~~~~ PL.y:316.33-39: warning: POSIX Yacc does not support string literals [-Wyacc] %token WHERE_TOK "WHERE" ^~~~~~~ PL.y:317.33-44: warning: POSIX Yacc does not support string literals [-Wyacc] %token ASSERTIONS_TOK "ASSERTIONS" ^~~~~~~~~~~~ PL.y:318.33-45: warning: POSIX Yacc does not support string literals [-Wyacc] %token ASSUMPTIONS_TOK "ASSUMPTIONS" ^~~~~~~~~~~~~ PL.y:319.33-48: warning: POSIX Yacc does not support string literals [-Wyacc] %token COUNTEREXAMPLE_TOK "COUNTEREXAMPLE" ^~~~~~~~~~~~~~~~ PL.y:320.33-46: warning: POSIX Yacc does not support string literals [-Wyacc] %token COUNTERMODEL_TOK "COUNTERMODEL" ^~~~~~~~~~~~~~ PL.y:321.33-38: warning: POSIX Yacc does not support string literals [-Wyacc] %token PUSH_TOK "PUSH" ^~~~~~ PL.y:322.33-37: warning: POSIX Yacc does not support string literals [-Wyacc] %token POP_TOK "POP" ^~~~~ PL.y:323.33-39: warning: POSIX Yacc does not support string literals [-Wyacc] %token POPTO_TOK "POPTO" ^~~~~~~ PL.y:324.33-44: warning: POSIX Yacc does not support string literals [-Wyacc] %token PUSH_SCOPE_TOK "PUSH_SCOPE" ^~~~~~~~~~~~ PL.y:325.33-43: warning: POSIX Yacc does not support string literals [-Wyacc] %token POP_SCOPE_TOK "POP_SCOPE" ^~~~~~~~~~~ PL.y:326.33-45: warning: POSIX Yacc does not support string literals [-Wyacc] %token POPTO_SCOPE_TOK "POPTO_SCOPE" ^~~~~~~~~~~~~ PL.y:327.33-39: warning: POSIX Yacc does not support string literals [-Wyacc] %token RESET_TOK "RESET" ^~~~~~~ PL.y:328.33-41: warning: POSIX Yacc does not support string literals [-Wyacc] %token CONTEXT_TOK "CONTEXT" ^~~~~~~~~ PL.y:329.33-40: warning: POSIX Yacc does not support string literals [-Wyacc] %token FORGET_TOK "FORGET" ^~~~~~~~ PL.y:330.33-42: warning: POSIX Yacc does not support string literals [-Wyacc] %token GET_TYPE_TOK "GET_TYPE" ^~~~~~~~~~ PL.y:331.33-44: warning: POSIX Yacc does not support string literals [-Wyacc] %token CHECK_TYPE_TOK "CHECK_TYPE" ^~~~~~~~~~~~ PL.y:332.33-43: warning: POSIX Yacc does not support string literals [-Wyacc] %token GET_CHILD_TOK "GET_CHILD" ^~~~~~~~~~~ PL.y:333.33-40: warning: POSIX Yacc does not support string literals [-Wyacc] %token GET_OP_TOK "GET_OP" ^~~~~~~~ PL.y:334.33-44: warning: POSIX Yacc does not support string literals [-Wyacc] %token SUBSTITUTE_TOK "SUBSTITUTE" ^~~~~~~~~~~~ PL.y: warning: 3 shift/reduce conflicts [-Wconflicts-sr] PL.y:1531.24-1536.25: warning: rule useless in parser due to conflicts [-Wother] AndExpr : AndExpr AND_TOK Expr ^~~~~~~~~~~~~ PL.y:1549.25-1554.25: warning: rule useless in parser due to conflicts [-Wother] OrExpr : OrExpr OR_TOK Expr ^~~~~~~~~~ flex -I -PLisp -olexLisp.cpp Lisp.lex flex -I -Psmtlib2 -olexsmtlib2.cpp smtlib2.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 parsesmtlib2.cpp lexsmtlib2.cpp parser.cpp g++ -M -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -O0 -I/usr/local/include parsePL.cpp lexPL.cpp parseLisp.cpp lexLisp.cpp parsesmtlib.cpp lexsmtlib.cpp parsesmtlib2.cpp lexsmtlib2.cpp parser.cpp >> /construction/math/cvc3/cvc3-2.4.1/obj/parser/x86_64-dragonfly5.5/Makefile.tmp g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -O0 -I/usr/local/include -c parsePL.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/parser/x86_64-dragonfly5.5/parsePL.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -O0 -I/usr/local/include -c lexLisp.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/parser/x86_64-dragonfly5.5/lexLisp.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -O0 -I/usr/local/include -c parseLisp.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/parser/x86_64-dragonfly5.5/parseLisp.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -O0 -I/usr/local/include -c lexPL.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/parser/x86_64-dragonfly5.5/lexPL.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -O0 -I/usr/local/include -c parsesmtlib.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/parser/x86_64-dragonfly5.5/parsesmtlib.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -O0 -I/usr/local/include -c lexsmtlib.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/parser/x86_64-dragonfly5.5/lexsmtlib.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -O0 -I/usr/local/include -c parsesmtlib2.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/parser/x86_64-dragonfly5.5/parsesmtlib2.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -O0 -I/usr/local/include -c lexsmtlib2.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/parser/x86_64-dragonfly5.5/lexsmtlib2.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -O0 -I/usr/local/include -c parser.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/parser/x86_64-dragonfly5.5/parser.o' ar ruvs '/construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libparser.a' /construction/math/cvc3/cvc3-2.4.1/obj/parser/x86_64-dragonfly5.5/parsePL.o /construction/math/cvc3/cvc3-2.4.1/obj/parser/x86_64-dragonfly5.5/lexPL.o /construction/math/cvc3/cvc3-2.4.1/obj/parser/x86_64-dragonfly5.5/parseLisp.o /construction/math/cvc3/cvc3-2.4.1/obj/parser/x86_64-dragonfly5.5/lexLisp.o /construction/math/cvc3/cvc3-2.4.1/obj/parser/x86_64-dragonfly5.5/parsesmtlib.o /construction/math/cvc3/cvc3-2.4.1/obj/parser/x86_64-dragonfly5.5/lexsmtlib.o /construction/math/cvc3/cvc3-2.4.1/obj/parser/x86_64-dragonfly5.5/parsesmtlib2.o /construction/math/cvc3/cvc3-2.4.1/obj/parser/x86_64-dragonfly5.5/lexsmtlib2.o /construction/math/cvc3/cvc3-2.4.1/obj/parser/x86_64-dragonfly5.5/parser.o /usr/libexec/binutils227/elf/ar: `u' modifier ignored since `D' is the default (see `U') /usr/libexec/binutils227/elf/ar: creating /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libparser.a a - /construction/math/cvc3/cvc3-2.4.1/obj/parser/x86_64-dragonfly5.5/parsePL.o a - /construction/math/cvc3/cvc3-2.4.1/obj/parser/x86_64-dragonfly5.5/lexPL.o a - /construction/math/cvc3/cvc3-2.4.1/obj/parser/x86_64-dragonfly5.5/parseLisp.o a - /construction/math/cvc3/cvc3-2.4.1/obj/parser/x86_64-dragonfly5.5/lexLisp.o a - /construction/math/cvc3/cvc3-2.4.1/obj/parser/x86_64-dragonfly5.5/parsesmtlib.o a - /construction/math/cvc3/cvc3-2.4.1/obj/parser/x86_64-dragonfly5.5/lexsmtlib.o a - /construction/math/cvc3/cvc3-2.4.1/obj/parser/x86_64-dragonfly5.5/parsesmtlib2.o a - /construction/math/cvc3/cvc3-2.4.1/obj/parser/x86_64-dragonfly5.5/lexsmtlib2.o a - /construction/math/cvc3/cvc3-2.4.1/obj/parser/x86_64-dragonfly5.5/parser.o gmake[3]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/parser' cd translator && gmake gmake[3]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/translator' Making dependencies for translator.cpp g++ -M -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include translator.cpp >> /construction/math/cvc3/cvc3-2.4.1/obj/translator/x86_64-dragonfly5.5/Makefile.tmp g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c translator.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/translator/x86_64-dragonfly5.5/translator.o' ar ruvs '/construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libtranslator.a' /construction/math/cvc3/cvc3-2.4.1/obj/translator/x86_64-dragonfly5.5/translator.o /usr/libexec/binutils227/elf/ar: `u' modifier ignored since `D' is the default (see `U') /usr/libexec/binutils227/elf/ar: creating /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libtranslator.a a - /construction/math/cvc3/cvc3-2.4.1/obj/translator/x86_64-dragonfly5.5/translator.o gmake[3]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/translator' cd vcl && gmake gmake[3]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/vcl' Making dependencies for vcl.cpp vc_cmd.cpp g++ -M -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include vcl.cpp vc_cmd.cpp >> /construction/math/cvc3/cvc3-2.4.1/obj/vcl/x86_64-dragonfly5.5/Makefile.tmp g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c vcl.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/vcl/x86_64-dragonfly5.5/vcl.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c vc_cmd.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/vcl/x86_64-dragonfly5.5/vc_cmd.o' vc_cmd.cpp: In member function 'bool CVC3::VCCmd::evaluateCommand(const CVC3::Expr&)': vc_cmd.cpp:780:10: warning: unused variable 'b' [-Wunused-variable] bool b = d_vc->inconsistent(assertions); ^ ar ruvs '/construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libvcl.a' /construction/math/cvc3/cvc3-2.4.1/obj/vcl/x86_64-dragonfly5.5/vcl.o /construction/math/cvc3/cvc3-2.4.1/obj/vcl/x86_64-dragonfly5.5/vc_cmd.o /usr/libexec/binutils227/elf/ar: `u' modifier ignored since `D' is the default (see `U') /usr/libexec/binutils227/elf/ar: creating /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libvcl.a a - /construction/math/cvc3/cvc3-2.4.1/obj/vcl/x86_64-dragonfly5.5/vcl.o a - /construction/math/cvc3/cvc3-2.4.1/obj/vcl/x86_64-dragonfly5.5/vc_cmd.o gmake[3]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/vcl' cd c_interface && gmake gmake[3]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/c_interface' Making dependencies for c_interface.cpp g++ -M -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include c_interface.cpp >> /construction/math/cvc3/cvc3-2.4.1/obj/c_interface/x86_64-dragonfly5.5/Makefile.tmp g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -I/usr/local/include -c c_interface.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/c_interface/x86_64-dragonfly5.5/c_interface.o' c_interface.cpp: In function 'void* vc_createValidityChecker(Flags)': c_interface.cpp:192:28: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch (CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_createFlags()': c_interface.cpp:202:28: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch (CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void vc_destroyValidityChecker(VC)': c_interface.cpp:214:28: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch (CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void vc_deleteFlags(Flags)': c_interface.cpp:223:28: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch (CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void vc_deleteExpr(Expr)': c_interface.cpp:233:28: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch (CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void vc_deleteVector(void**)': c_interface.cpp:255:28: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch (CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void vc_setBoolFlag(Flags, char*, int)': c_interface.cpp:271:28: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch (CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void vc_setIntFlag(Flags, char*, int)': c_interface.cpp:281:28: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch (CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void vc_setStringFlag(Flags, char*, char*)': c_interface.cpp:291:28: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch (CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void vc_setStrSeqFlag(Flags, char*, char*, int)': c_interface.cpp:301:28: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch (CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_boolType(VC)': c_interface.cpp:312:28: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch (CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_realType(VC)': c_interface.cpp:324:27: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch (CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_intType(VC)': c_interface.cpp:336:27: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch (CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_tupleType2(VC, Type, Type)': c_interface.cpp:373:27: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch (CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_tupleType3(VC, Type, Type, Type)': c_interface.cpp:386:27: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch (CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_tupleTypeN(VC, void**, int)': c_interface.cpp:402:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_recordType1(VC, char*, Type)': c_interface.cpp:414:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_recordType2(VC, char*, Type, char*, Type)': c_interface.cpp:428:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_recordType3(VC, char*, Type, char*, Type, char*, Type)': c_interface.cpp:444:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_recordTypeN(VC, char**, void**, int)': c_interface.cpp:463:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_dataType1(VC, char*, char*, int, char**, void**)': c_interface.cpp:484:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_dataTypeN(VC, char*, int, char**, int*, char***, void***)': c_interface.cpp:509:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void** vc_dataTypeMN(VC, int, char**, int*, char***, int**, char****, void****)': c_interface.cpp:548:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_arrayType(VC, Type, Type)': c_interface.cpp:560:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_bvType(VC, int)': c_interface.cpp:572:27: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch (CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_funType1(VC, Type, Type)': c_interface.cpp:584:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_funType2(VC, Type, Type, Type)': c_interface.cpp:599:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_funType3(VC, Type, Type, Type, Type)': c_interface.cpp:615:27: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_funTypeN(VC, void**, Type, int)': c_interface.cpp:630:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_createType(VC, char*)': c_interface.cpp:642:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_lookupType(VC, char*)': c_interface.cpp:654:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_getEM(VC)': c_interface.cpp:671:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_varExpr(VC, char*, Type)': c_interface.cpp:683:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_varExprDef(VC, char*, Type, Expr)': c_interface.cpp:695:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_lookupVar(VC, char*, void**)': c_interface.cpp:710:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_getType(VC, Expr)': c_interface.cpp:722:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_getBaseType(VC, Expr)': c_interface.cpp:734:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_getBaseTypeOfType(VC, Type)': c_interface.cpp:746:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_getTypePred(VC, Type, Expr)': c_interface.cpp:758:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_stringExpr(VC, char*)': c_interface.cpp:770:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_idExpr(VC, char*)': c_interface.cpp:782:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_listExpr(VC, int, void**)': c_interface.cpp:797:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void vc_printExpr(VC, Expr)': c_interface.cpp:809:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'char* vc_printExprString(VC, Expr)': c_interface.cpp:828:27: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch(CVC3::Exception ex) { ^~ c_interface.cpp: In function 'void vc_printExprFile(VC, Expr, int)': c_interface.cpp:850:27: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch(CVC3::Exception ex) { ^~ c_interface.cpp: In function 'void* vc_importExpr(VC, Expr)': c_interface.cpp:861:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_importType(VC, Type)': c_interface.cpp:873:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_eqExpr(VC, Expr, Expr)': c_interface.cpp:885:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_distinctExpr(VC, void**, int)': c_interface.cpp:900:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_trueExpr(VC)': c_interface.cpp:912:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_falseExpr(VC)': c_interface.cpp:924:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_notExpr(VC, Expr)': c_interface.cpp:936:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_andExpr(VC, Expr, Expr)': c_interface.cpp:948:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_andExprN(VC, void**, int)': c_interface.cpp:964:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_orExpr(VC, Expr, Expr)': c_interface.cpp:976:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_orExprN(VC, void**, int)': c_interface.cpp:992:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_impliesExpr(VC, Expr, Expr)': c_interface.cpp:1004:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_iffExpr(VC, Expr, Expr)': c_interface.cpp:1016:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_iteExpr(VC, Expr, Expr, Expr)': c_interface.cpp:1029:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_substExpr(VC, Expr, void**, int, void**, int)': c_interface.cpp:1051:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_createOp(VC, char*, Type)': c_interface.cpp:1064:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_createOpDef(VC, char*, Type, Expr)': c_interface.cpp:1076:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_lookupOp(VC, char*, void**)': c_interface.cpp:1091:27: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_funExpr1(VC, Op, Expr)': c_interface.cpp:1103:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_funExpr2(VC, Op, Expr, Expr)': c_interface.cpp:1115:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_funExpr3(VC, Op, Expr, Expr, Expr)': c_interface.cpp:1129:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_funExprN(VC, Op, void**, int)': c_interface.cpp:1145:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_ratExpr(VC, int, int)': c_interface.cpp:1157:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_ratExprFromStr(VC, char*, char*, int)': c_interface.cpp:1169:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_ratExprFromStr1(VC, char*, int)': c_interface.cpp:1181:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_uminusExpr(VC, Expr)': c_interface.cpp:1193:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_plusExpr(VC, Expr, Expr)': c_interface.cpp:1205:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_plusExprN(VC, void**, int)': c_interface.cpp:1220:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_minusExpr(VC, Expr, Expr)': c_interface.cpp:1232:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_multExpr(VC, Expr, Expr)': c_interface.cpp:1244:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_powExpr(VC, Expr, Expr)': c_interface.cpp:1256:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_divideExpr(VC, Expr, Expr)': c_interface.cpp:1268:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_ltExpr(VC, Expr, Expr)': c_interface.cpp:1280:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_leExpr(VC, Expr, Expr)': c_interface.cpp:1292:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_gtExpr(VC, Expr, Expr)': c_interface.cpp:1304:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_geExpr(VC, Expr, Expr)': c_interface.cpp:1316:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_recordExpr1(VC, char*, Expr)': c_interface.cpp:1328:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_recordExpr2(VC, char*, Expr, char*, Expr)': c_interface.cpp:1342:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_recordExpr3(VC, char*, Expr, char*, Expr, char*, Expr)': c_interface.cpp:1358:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_recordExprN(VC, char**, void**, int)': c_interface.cpp:1377:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_recSelectExpr(VC, Expr, char*)': c_interface.cpp:1389:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_recUpdateExpr(VC, Expr, char*, Expr)': c_interface.cpp:1403:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_readExpr(VC, Expr, Expr)': c_interface.cpp:1415:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_writeExpr(VC, Expr, Expr, Expr)': c_interface.cpp:1428:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_bvConstExprFromStr(VC, char*)': c_interface.cpp:1446:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_bvExtract(VC, Expr, int, int)': c_interface.cpp:1504:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_bvBoolExtract(VC, Expr, int)': c_interface.cpp:1518:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_bvNotExpr(VC, Expr)': c_interface.cpp:1530:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_bvAndExpr(VC, Expr, Expr)': c_interface.cpp:1542:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_bvOrExpr(VC, Expr, Expr)': c_interface.cpp:1554:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_bvXorExpr(VC, Expr, Expr)': c_interface.cpp:1566:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_bvLtExpr(VC, Expr, Expr)': c_interface.cpp:1578:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_bvLeExpr(VC, Expr, Expr)': c_interface.cpp:1590:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_bvGtExpr(VC, Expr, Expr)': c_interface.cpp:1604:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_bvGeExpr(VC, Expr, Expr)': c_interface.cpp:1618:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_bvSLtExpr(VC, Expr, Expr)': c_interface.cpp:1630:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_bvSLeExpr(VC, Expr, Expr)': c_interface.cpp:1642:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_bvSGtExpr(VC, Expr, Expr)': c_interface.cpp:1656:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_bvSGeExpr(VC, Expr, Expr)': c_interface.cpp:1670:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_bvSignExtend(VC, Expr, int)': c_interface.cpp:1682:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_bvUMinusExpr(VC, Expr)': c_interface.cpp:1694:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_bvPlusExpr(VC, int, Expr, Expr)': c_interface.cpp:1709:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_bvMinusExpr(VC, int, Expr, Expr)': c_interface.cpp:1728:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_bvMultExpr(VC, int, Expr, Expr)': c_interface.cpp:1746:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_bvLeftShiftExpr(VC, int, Expr)': c_interface.cpp:1764:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_bvRightShiftExpr(VC, int, Expr)': c_interface.cpp:1776:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_bvUDivExpr(VC, Expr, Expr)': c_interface.cpp:1787:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_bvURemExpr(VC, Expr, Expr)': c_interface.cpp:1798:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_bvSDivExpr(VC, Expr, Expr)': c_interface.cpp:1809:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_bvSRemExpr(VC, Expr, Expr)': c_interface.cpp:1820:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_bvSModExpr(VC, Expr, Expr)': c_interface.cpp:1831:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_bvVar32LeftShiftExpr(VC, Expr, Expr)': c_interface.cpp:1871:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_bvVar32DivByPowOfTwoExpr(VC, Expr, Expr)': c_interface.cpp:1897:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_bvVar32RightShiftExpr(VC, Expr, Expr)': c_interface.cpp:1924:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_bvWriteToMemoryArray(VC, Expr, Expr, Expr, int)': c_interface.cpp:2043:9: warning: variable 'hi' set but not used [-Wunused-but-set-variable] int hi = newBitsPerElem - 1; ^~ c_interface.cpp: In function 'void* vc_tupleExprN(VC, void**, int)': c_interface.cpp:2076:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_tupleSelectExpr(VC, Expr, int)': c_interface.cpp:2088:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_tupleUpdateExpr(VC, Expr, int, Expr)': c_interface.cpp:2101:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_datatypeConsExpr(VC, char*, int, void**)': c_interface.cpp:2118:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_datatypeSelExpr(VC, char*, Expr)': c_interface.cpp:2130:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_datatypeTestExpr(VC, char*, Expr)': c_interface.cpp:2142:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_boundVarExpr(VC, char*, char*, Type)': c_interface.cpp:2154:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_forallExpr(VC, void**, int, Expr)': c_interface.cpp:2170:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void vc_setTriggers(VC, Expr, int, void**)': c_interface.cpp:2199:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_existsExpr(VC, void**, int, Expr)': c_interface.cpp:2214:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_lambdaExpr(VC, int, void**, Expr)': c_interface.cpp:2230:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void vc_setResourceLimit(VC, unsigned int)': c_interface.cpp:2247:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void vc_assertFormula(VC, Expr)': c_interface.cpp:2258:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void vc_registerAtom(VC, Expr)': c_interface.cpp:2269:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_getImpliedLiteral(VC)': c_interface.cpp:2280:27: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_simplify(VC, Expr)': c_interface.cpp:2292:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'int vc_query(VC, Expr)': c_interface.cpp:2304:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'int vc_checkContinue(VC)': c_interface.cpp:2316:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'int vc_restart(VC, Expr)': c_interface.cpp:2328:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void vc_returnFromCheck(VC)': c_interface.cpp:2340:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void** vc_getUserAssumptions(VC, int*)': c_interface.cpp:2359:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void** vc_getInternalAssumptions(VC, int*)': c_interface.cpp:2379:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void** vc_getAssumptions(VC, int*)': c_interface.cpp:2399:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_getProofAssumptions(VC)': c_interface.cpp:2413:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_getProofQuery(VC)': c_interface.cpp:2425:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void** vc_getAssumptionsUsed(VC, int*)': c_interface.cpp:2445:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void** vc_getCounterExample(VC, int*)': c_interface.cpp:2465:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void** vc_getConcreteModel(VC, int*)': c_interface.cpp:2487:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'int vc_inconsistent(VC, void***, int*)': c_interface.cpp:2507:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'char* vc_incomplete(VC)': c_interface.cpp:2530:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_getProof(VC)': c_interface.cpp:2542:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_getProofOfFile(VC, char*)': c_interface.cpp:2563:28: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch (CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_getTCC(VC)': c_interface.cpp:2575:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void** vc_getAssumptionsTCC(VC, int*)': c_interface.cpp:2595:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_getProofTCC(VC)': c_interface.cpp:2607:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_getClosure(VC)': c_interface.cpp:2619:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_getProofClosure(VC)': c_interface.cpp:2631:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'int vc_stackLevel(VC)': c_interface.cpp:2643:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void vc_push(VC)': c_interface.cpp:2655:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void vc_pop(VC)': c_interface.cpp:2666:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void vc_popto(VC, int)': c_interface.cpp:2677:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'int vc_compare_exprs(Expr, Expr)': c_interface.cpp:2698:28: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch (CVC3::Exception ex){ ^~ c_interface.cpp: In function 'const char* vc_exprString(Expr)': c_interface.cpp:2709:28: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch (CVC3::Exception ex){ ^~ c_interface.cpp: In function 'const char* vc_typeString(Type)': c_interface.cpp:2720:28: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch (CVC3::Exception ex){ ^~ c_interface.cpp: In function 'bool vc_isClosure(Expr)': c_interface.cpp:2730:28: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch (CVC3::Exception ex){ ^~ c_interface.cpp: In function 'bool vc_isQuantifier(Expr)': c_interface.cpp:2740:28: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch (CVC3::Exception ex){ ^~ c_interface.cpp: In function 'bool vc_isLambda(Expr)': c_interface.cpp:2750:28: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch (CVC3::Exception ex){ ^~ c_interface.cpp: In function 'bool vc_isVar(Expr)': c_interface.cpp:2760:28: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch (CVC3::Exception ex){ ^~ c_interface.cpp: In function 'int vc_arity(Expr)': c_interface.cpp:2770:28: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch (CVC3::Exception ex){ ^~ c_interface.cpp: In function 'int vc_getKind(Expr)': c_interface.cpp:2780:28: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch (CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_getChild(Expr, int)': c_interface.cpp:2790:28: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch (CVC3::Exception ex){ ^~ c_interface.cpp: In function 'int vc_getNumVars(Expr)': c_interface.cpp:2800:28: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch (CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_getVar(Expr, int)': c_interface.cpp:2816:28: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch (CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_getBody(Expr)': c_interface.cpp:2826:28: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch (CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_getExistential(Expr)': c_interface.cpp:2835:28: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch (CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_getFun(VC, Expr)': c_interface.cpp:2846:26: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] }catch(CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void* vc_toExpr(Type)': c_interface.cpp:2856:28: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch (CVC3::Exception ex){ ^~ c_interface.cpp: In function 'const char* vc_getKindString(VC, int)': c_interface.cpp:2869:28: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch (CVC3::Exception ex){ ^~ c_interface.cpp: In function 'int vc_getKindInt(VC, char*)': c_interface.cpp:2881:28: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch (CVC3::Exception ex){ ^~ c_interface.cpp: In function 'int vc_getInt(Expr)': c_interface.cpp:2891:28: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch (CVC3::Exception ex){ ^~ c_interface.cpp: In function 'int vc_getBVInt(VC, Expr)': c_interface.cpp:2902:28: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch (CVC3::Exception ex){ ^~ c_interface.cpp: In function 'unsigned int vc_getBVUnsigned(VC, Expr)': c_interface.cpp:2913:28: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch (CVC3::Exception ex){ ^~ c_interface.cpp: In function 'void vc_print_statistics(VC)': c_interface.cpp:2925:28: warning: catching polymorphic type 'class CVC3::Exception' by value [-Wcatch-value=] } catch (CVC3::Exception ex){ ^~ ar ruvs '/construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libc_interface.a' /construction/math/cvc3/cvc3-2.4.1/obj/c_interface/x86_64-dragonfly5.5/c_interface.o /usr/libexec/binutils227/elf/ar: `u' modifier ignored since `D' is the default (see `U') /usr/libexec/binutils227/elf/ar: creating /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libc_interface.a a - /construction/math/cvc3/cvc3-2.4.1/obj/c_interface/x86_64-dragonfly5.5/c_interface.o gmake[3]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/c_interface' gmake /construction/math/cvc3/cvc3-2.4.1/lib/libcvc3.so.5.0.0 gmake[3]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src' Building shared library /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libcvc3.so.5.0.0 rm -rf /construction/math/cvc3/cvc3-2.4.1/unpack_tmp /construction/math/cvc3/cvc3-2.4.1/bin/unpack /construction/math/cvc3/cvc3-2.4.1/unpack_tmp /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libcvc_util.a /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libcontext.a /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libexpr.a /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libtheorem.a /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libsat.a /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libtheory_core.a /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libtheory_arith.a /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libtheory_array.a /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libtheory_bitvector.a /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libtheory_datatype.a /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libtheory_quant.a /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libtheory_records.a /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libtheory_simulate.a /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libtheory_uf.a /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libsearch.a /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libparser.a /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libtranslator.a /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libvcl.a /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libc_interface.a > UNPACKED Found 90 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 -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -L/usr/local/lib \ -Wl,-soname,libcvc3.so.5 -o '/construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libcvc3.so.5.0.0' `` -lgmp ln -sf libcvc3.so.5.0.0 /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libcvc3.so.5.0 ln -sf libcvc3.so.5.0.0 /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libcvc3.so.5 ln -sf libcvc3.so.5.0.0 /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libcvc3.so ln -sf /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libcvc3.so.5.0.0 '/construction/math/cvc3/cvc3-2.4.1/lib//libcvc3.so.5.0.0' ln -sf libcvc3.so.5.0.0 '/construction/math/cvc3/cvc3-2.4.1/lib//libcvc3.so.5.0' ln -sf libcvc3.so.5.0.0 '/construction/math/cvc3/cvc3-2.4.1/lib//libcvc3.so.5' ln -sf libcvc3.so.5.0.0 '/construction/math/cvc3/cvc3-2.4.1/lib//libcvc3.so' gmake[3]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src' cd cvc3 && gmake VERSION=2.4.1 gmake[3]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/cvc3' Making dependencies for main.cpp g++ -M -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DVERSION=\"2.4.1\" -I/usr/local/include main.cpp >> /construction/math/cvc3/cvc3-2.4.1/obj/cvc3/x86_64-dragonfly5.5/Makefile.tmp gmake /construction/math/cvc3/cvc3-2.4.1/bin/x86_64-dragonfly5.5/cvc3 gmake[4]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/cvc3' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DVERSION=\"2.4.1\" -I/usr/local/include -c main.cpp -o '/construction/math/cvc3/cvc3-2.4.1/obj/cvc3/x86_64-dragonfly5.5/main.o' g++ -pipe -O2 -fno-strict-aliasing -fPIC -std=gnu++98 -m64 -fPIC -O2 -Wall -I. -I/construction/math/cvc3/cvc3-2.4.1/src/include -DVERSION=\"2.4.1\" -L/usr/local/lib -o '/construction/math/cvc3/cvc3-2.4.1/bin/x86_64-dragonfly5.5/cvc3' /construction/math/cvc3/cvc3-2.4.1/obj/cvc3/x86_64-dragonfly5.5/main.o \ -L/construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5 -lcvc3 -lgmp gmake[4]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/cvc3' ln -sf /construction/math/cvc3/cvc3-2.4.1/bin/x86_64-dragonfly5.5/cvc3 /construction/math/cvc3/cvc3-2.4.1/bin/cvc3 gmake[3]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/cvc3' gmake[2]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src' find /construction/math/cvc3/cvc3-2.4.1/src '(' -name "*.h" -o -name "*.cpp" -o \ -name "*.y" ')' \ ! -name "lexPL.cpp" ! -name "parsePL.cpp" \ -print > FILES gmake[1]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1' -------------------------------------------------------------------------------- -- Phase: run-depends -------------------------------------------------------------------------------- ===> cvc3-2.4.1_6 depends on package: perl5>=5.28.r1<5.29 - found -------------------------------------------------------------------------------- -- Phase: stage -------------------------------------------------------------------------------- ===> Staging for cvc3-2.4.1_6 ===> Generating temporary packing list gmake[1]: Entering directory '/construction/math/cvc3/cvc3-2.4.1' gmake TARGET=install gmake[2]: Entering directory '/construction/math/cvc3/cvc3-2.4.1' cd /construction/math/cvc3/cvc3-2.4.1/src; gmake install VERSION=2.4.1 gmake[3]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src' gmake build TARGET= gmake[4]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src' cd util && gmake gmake[5]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/util' gmake[5]: Nothing to be done for 'all'. gmake[5]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/util' cd context && gmake gmake[5]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/context' gmake[5]: Nothing to be done for 'all'. gmake[5]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/context' cd expr && gmake gmake[5]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/expr' gmake[5]: Nothing to be done for 'all'. gmake[5]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/expr' cd theorem && gmake gmake[5]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/theorem' gmake[5]: Nothing to be done for 'all'. gmake[5]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/theorem' cd sat && gmake gmake[5]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/sat' gmake[5]: Nothing to be done for 'all'. gmake[5]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/sat' cd theory_core && gmake gmake[5]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/theory_core' gmake[5]: Nothing to be done for 'all'. gmake[5]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/theory_core' cd theory_arith && gmake gmake[5]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/theory_arith' gmake[5]: Nothing to be done for 'all'. gmake[5]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/theory_arith' cd theory_array && gmake gmake[5]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/theory_array' gmake[5]: Nothing to be done for 'all'. gmake[5]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/theory_array' cd theory_bitvector && gmake gmake[5]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/theory_bitvector' gmake[5]: Nothing to be done for 'all'. gmake[5]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/theory_bitvector' cd theory_datatype && gmake gmake[5]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/theory_datatype' gmake[5]: Nothing to be done for 'all'. gmake[5]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/theory_datatype' cd theory_quant && gmake gmake[5]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/theory_quant' gmake[5]: Nothing to be done for 'all'. gmake[5]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/theory_quant' cd theory_records && gmake gmake[5]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/theory_records' gmake[5]: Nothing to be done for 'all'. gmake[5]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/theory_records' cd theory_simulate && gmake gmake[5]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/theory_simulate' gmake[5]: Nothing to be done for 'all'. gmake[5]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/theory_simulate' cd theory_uf && gmake gmake[5]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/theory_uf' gmake[5]: Nothing to be done for 'all'. gmake[5]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/theory_uf' cd search && gmake gmake[5]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/search' gmake[5]: Nothing to be done for 'all'. gmake[5]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/search' cd parser && gmake gmake[5]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/parser' gmake[5]: Nothing to be done for 'all'. gmake[5]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/parser' cd translator && gmake gmake[5]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/translator' gmake[5]: Nothing to be done for 'all'. gmake[5]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/translator' cd vcl && gmake gmake[5]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/vcl' gmake[5]: Nothing to be done for 'all'. gmake[5]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/vcl' cd c_interface && gmake gmake[5]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/c_interface' gmake[5]: Nothing to be done for 'all'. gmake[5]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/c_interface' gmake /construction/math/cvc3/cvc3-2.4.1/lib/libcvc3.so.5.0.0 gmake[5]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src' ln -sf /construction/math/cvc3/cvc3-2.4.1/lib/x86_64-dragonfly5.5/libcvc3.so.5.0.0 '/construction/math/cvc3/cvc3-2.4.1/lib//libcvc3.so.5.0.0' ln -sf libcvc3.so.5.0.0 '/construction/math/cvc3/cvc3-2.4.1/lib//libcvc3.so.5.0' ln -sf libcvc3.so.5.0.0 '/construction/math/cvc3/cvc3-2.4.1/lib//libcvc3.so.5' ln -sf libcvc3.so.5.0.0 '/construction/math/cvc3/cvc3-2.4.1/lib//libcvc3.so' gmake[5]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src' cd cvc3 && gmake VERSION=2.4.1 gmake[5]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/cvc3' gmake /construction/math/cvc3/cvc3-2.4.1/bin/x86_64-dragonfly5.5/cvc3 gmake[6]: Entering directory '/construction/math/cvc3/cvc3-2.4.1/src/cvc3' gmake[6]: '/construction/math/cvc3/cvc3-2.4.1/bin/x86_64-dragonfly5.5/cvc3' is up to date. gmake[6]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/cvc3' ln -sf /construction/math/cvc3/cvc3-2.4.1/bin/x86_64-dragonfly5.5/cvc3 /construction/math/cvc3/cvc3-2.4.1/bin/cvc3 gmake[5]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src/cvc3' gmake[4]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src' mkdir -p /construction/math/cvc3/stage/usr/local/include/cvc3 /usr/bin/install -c -m 644 /construction/math/cvc3/cvc3-2.4.1/src/include/assumptions.h /construction/math/cvc3/cvc3-2.4.1/src/include/c_interface.h /construction/math/cvc3/cvc3-2.4.1/src/include/c_interface_defs.h /construction/math/cvc3/cvc3-2.4.1/src/include/cdflags.h /construction/math/cvc3/cvc3-2.4.1/src/include/cdlist.h /construction/math/cvc3/cvc3-2.4.1/src/include/cdmap.h /construction/math/cvc3/cvc3-2.4.1/src/include/cdmap_ordered.h /construction/math/cvc3/cvc3-2.4.1/src/include/cdo.h /construction/math/cvc3/cvc3-2.4.1/src/include/circuit.h /construction/math/cvc3/cvc3-2.4.1/src/include/clause.h /construction/math/cvc3/cvc3-2.4.1/src/include/cnf.h /construction/math/cvc3/cvc3-2.4.1/src/include/cnf_manager.h /construction/math/cvc3/cvc3-2.4.1/src/include/command_line_exception.h /construction/math/cvc3/cvc3-2.4.1/src/include/command_line_flags.h /construction/math/cvc3/cvc3-2.4.1/src/include/common_proof_rules.h /construction/math/cvc3/cvc3-2.4.1/src/include/compat_hash_map.h /construction/math/cvc3/cvc3-2.4.1/src/include/compat_hash_set.h /construction/math/cvc3/cvc3-2.4.1/src/include/context.h /construction/math/cvc3/cvc3-2.4.1/src/include/cvc_util.h /construction/math/cvc3/cvc3-2.4.1/src/include/debug.h /construction/math/cvc3/cvc3-2.4.1/src/include/dpllt.h /construction/math/cvc3/cvc3-2.4.1/src/include/dpllt_basic.h /construction/math/cvc3/cvc3-2.4.1/src/include/dpllt_minisat.h /construction/math/cvc3/cvc3-2.4.1/src/include/eval_exception.h /construction/math/cvc3/cvc3-2.4.1/src/include/exception.h /construction/math/cvc3/cvc3-2.4.1/src/include/expr.h /construction/math/cvc3/cvc3-2.4.1/src/include/expr_hash.h /construction/math/cvc3/cvc3-2.4.1/src/include/expr_manager.h /construction/math/cvc3/cvc3-2.4.1/src/include/expr_map.h /construction/math/cvc3/cvc3-2.4.1/src/include/expr_op.h /construction/math/cvc3/cvc3-2.4.1/src/include/expr_stream.h /construction/math/cvc3/cvc3-2.4.1/src/include/expr_transform.h /construction/math/cvc3/cvc3-2.4.1/src/include/expr_value.h /construction/math/cvc3/cvc3-2.4.1/src/include/formula_value.h /construction/math/cvc3/cvc3-2.4.1/src/include/fdstream.h /construction/math/cvc3/cvc3-2.4.1/src/include/hash_fun.h /construction/math/cvc3/cvc3-2.4.1/src/include/hash_table.h /construction/math/cvc3/cvc3-2.4.1/src/include/hash_map.h /construction/math/cvc3/cvc3-2.4.1/src/include/hash_set.h /construction/math/cvc3/cvc3-2.4.1/src/include/kinds.h /construction/math/cvc3/cvc3-2.4.1/src/include/lang.h /construction/math/cvc3/cvc3-2.4.1/src/include/memory_manager.h /construction/math/cvc3/cvc3-2.4.1/src/include/memory_manager_chunks.h /construction/math/cvc3/cvc3-2.4.1/src/include/memory_manager_malloc.h /construction/math/cvc3/cvc3-2.4.1/src/include/memory_manager_context.h /construction/math/cvc3/cvc3-2.4.1/src/include/notifylist.h /construction/math/cvc3/cvc3-2.4.1/src/include/os.h /construction/math/cvc3/cvc3-2.4.1/src/include/parser.h /construction/math/cvc3/cvc3-2.4.1/src/include/proof.h /construction/math/cvc3/cvc3-2.4.1/src/include/rational.h /construction/math/cvc3/cvc3-2.4.1/src/include/parser_exception.h /construction/math/cvc3/cvc3-2.4.1/src/include/pretty_printer.h /construction/math/cvc3/cvc3-2.4.1/src/include/queryresult.h /construction/math/cvc3/cvc3-2.4.1/src/include/sat_api.h /construction/math/cvc3/cvc3-2.4.1/src/include/search.h /construction/math/cvc3/cvc3-2.4.1/src/include/search_impl_base.h /construction/math/cvc3/cvc3-2.4.1/src/include/search_sat.h /construction/math/cvc3/cvc3-2.4.1/src/include/search_simple.h /construction/math/cvc3/cvc3-2.4.1/src/include/search_fast.h /construction/math/cvc3/cvc3-2.4.1/src/include/smartcdo.h /construction/math/cvc3/cvc3-2.4.1/src/include/smtlib_exception.h /construction/math/cvc3/cvc3-2.4.1/src/include/sound_exception.h /construction/math/cvc3/cvc3-2.4.1/src/include/statistics.h /construction/math/cvc3/cvc3-2.4.1/src/include/theorem.h /construction/math/cvc3/cvc3-2.4.1/src/include/theorem_manager.h /construction/math/cvc3/cvc3-2.4.1/src/include/theorem_producer.h /construction/math/cvc3/cvc3-2.4.1/src/include/theory_arith.h /construction/math/cvc3/cvc3-2.4.1/src/include/theory_arith_new.h /construction/math/cvc3/cvc3-2.4.1/src/include/theory_arith_old.h /construction/math/cvc3/cvc3-2.4.1/src/include/theory_arith3.h /construction/math/cvc3/cvc3-2.4.1/src/include/theory_array.h /construction/math/cvc3/cvc3-2.4.1/src/include/theory_bitvector.h /construction/math/cvc3/cvc3-2.4.1/src/include/theory_core.h /construction/math/cvc3/cvc3-2.4.1/src/include/theory_datatype.h /construction/math/cvc3/cvc3-2.4.1/src/include/theory_datatype_lazy.h /construction/math/cvc3/cvc3-2.4.1/src/include/theory.h /construction/math/cvc3/cvc3-2.4.1/src/include/theory_quant.h /construction/math/cvc3/cvc3-2.4.1/src/include/theory_records.h /construction/math/cvc3/cvc3-2.4.1/src/include/theory_simulate.h /construction/math/cvc3/cvc3-2.4.1/src/include/theory_uf.h /construction/math/cvc3/cvc3-2.4.1/src/include/translator.h /construction/math/cvc3/cvc3-2.4.1/src/include/typecheck_exception.h /construction/math/cvc3/cvc3-2.4.1/src/include/type.h /construction/math/cvc3/cvc3-2.4.1/src/include/variable.h /construction/math/cvc3/cvc3-2.4.1/src/include/vc_cmd.h /construction/math/cvc3/cvc3-2.4.1/src/include/vc.h /construction/math/cvc3/cvc3-2.4.1/src/include/vcl.h /construction/math/cvc3/stage/usr/local/include/cvc3 mkdir -p /construction/math/cvc3/stage/usr/local/lib /usr/bin/install -c -m 644 /construction/math/cvc3/cvc3-2.4.1/lib/libcvc3.so.5.0.0 /construction/math/cvc3/stage/usr/local/lib ln -sf libcvc3.so.5.0.0 /construction/math/cvc3/stage/usr/local/lib/libcvc3.so.5.0 ln -sf libcvc3.so.5.0.0 /construction/math/cvc3/stage/usr/local/lib/libcvc3.so.5 ln -sf libcvc3.so.5.0.0 /construction/math/cvc3/stage/usr/local/lib/libcvc3.so mkdir -p /construction/math/cvc3/stage/usr/local/bin /usr/bin/install -c -m 755 /construction/math/cvc3/cvc3-2.4.1/bin/cvc3 /construction/math/cvc3/stage/usr/local/bin mkdir -p /construction/math/cvc3/stage/usr/local/libdata/pkgconfig /usr/bin/install -c -m 644 cvc3.pc /construction/math/cvc3/stage/usr/local/libdata/pkgconfig gmake[3]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1/src' gmake[2]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1' gmake[1]: Leaving directory '/construction/math/cvc3/cvc3-2.4.1' install -s -m 555 `readlink /construction/math/cvc3/cvc3-2.4.1/bin/cvc3` /construction/math/cvc3/stage/usr/local/bin /usr/bin/strip /construction/math/cvc3/stage/usr/local/lib/libcvc3.so.5.0.0 ====> Compressing man pages (compress-man) -------------------------------------------------------------------------------- -- Phase: package -------------------------------------------------------------------------------- ===> Building package for cvc3-2.4.1_6 file sizes/checksums [93]: . done packing files [93]: . done packing directories [0]: . done -------------------------------------------------- -- Termination -------------------------------------------------- Finished: Friday, 8 MAR 2019 at 18:06:05 UTC Duration: 00:05:41