Skip to content

Instantly share code, notes, and snippets.

@Coda-Coda

Coda-Coda/nix-shell error with archetype

Last active September 24, 2020 10:13
Show Gist options
  • Save Coda-Coda/5456b59cfbced6b61c8f50aa48d41aff to your computer and use it in GitHub Desktop.
Save Coda-Coda/5456b59cfbced6b61c8f50aa48d41aff to your computer and use it in GitHub Desktop.
Download ZIP
Nix-shell error with Archetype
Raw
nix-shell error with archetype
# Relates to https://github.com/timbertson/opam2nix/issues/43
# Ran on Ubuntu on AWS
$ nix-shell
ERROR: ld.so: object 'libgtk3-nocsd.so.0' from LD_PRELOAD cannot be preloaded (cannot open shared object file): ignored.
trace: [wrangle] Providing source self (git-local) from /nix/store/d2pcpfs5cvw913rw7jk8hpnc4ssg39rk-dbgihl2pv3yh1jbi1k68sgdy0kp5d467-source
trace: [wrangle] Providing source cudf (url) from /nix/store/3r17n7vjrbihzr7z0cd163xvzxz6mx4w-cudf-0.9.tar.gz
trace: [wrangle] Providing source dose (url) from /nix/store/mh2jr4sgghybljmfk7wlynn2pwq3ccfn-dose3-5.0.1.tar.gz
trace: [wrangle] Providing source mccs (url) from /nix/store/1ssag69f74snzkk53cwr1alwkil7a1lc-1.1+9.tar.gz
trace: [wrangle] Providing source opam (github) from /nix/store/s26wnykrfqxkpj1iy1vkh69nz9j0axgi-source
trace: [wrangle] Providing source opam-file-format (github) from /nix/store/kpk45bmqdrm3p43ac1bcsbr3yh5yrkpz-source
these derivations will be built:
/nix/store/0ck9b94sxx4aya9n60711ca2yqd0i4zr-source.drv
/nix/store/85cmdzf6pp8ga8kann7pkygjmi7s79xc-setupHook.sh.drv
/nix/store/cn5h562yks2mp6gvv8kwh7g98akvfgfp-ocaml-path-hooks.drv
/nix/store/c7dc7a04zj9zf04hyj3p78rzd2213xkd-source.drv
/nix/store/h0mafbpnsi0n2d4pvd1cq1s6lrpahvvn-opam.drv
/nix/store/c190smlhsc8la5id4j1njwpl5pqvhqr3-source.drv
/nix/store/41mw6cc35jdnmdid4bw527ha4067z58v-opam-file-format.drv
/nix/store/jrm3yd1i29byczb85akwv89zf6zhl395-ocamlgraph-1.8.8.drv
/nix/store/lsaj8fhckhbinifkffa22mf512n0nzxz-ocaml4.08.1-opam-core-dev.drv
/nix/store/hqsin8p5kcllpvmihb0w7ybkawsw61qi-ocaml4.08.1-opam-format-dev.drv
/nix/store/3mvkbahprfzs3kjyx4jmxvyyfg75smws-ocaml4.08.1-opam-installer-dev.drv
/nix/store/cp4jsla12z2avm8bckymk4nw80h0djw3-ocaml4.08.1-opam-repository-dev.drv
/nix/store/4whdi9zz173wl3gwnv14cjgy6y254hzj-ocaml4.08.1-opam-state-dev.drv
/nix/store/pmylsz2shy00i5f0wpl5p16msadf57x3-ocaml4.08.1-lwt_ppx-2.0.1.drv
/nix/store/6nz0mjkqyf49bkwblp7plgjgnrcp2ja8-ocurl-0.9.1.drv
/nix/store/nqkib5lzcxl80f1gnqyzmp664190pikp-ocaml4.08.1-fileutils-0.5.3.drv
/nix/store/1092sn9v9wd7p1d9i3rgj9ssm0ajxppv-ocaml4.08.1-extlib-1.7.6.drv
/nix/store/j0fcr59bnpc5k5h20l3hwq0j5k0d4pqi-cudf.drv
/nix/store/8zsnr0ff0wg6kkxm24b24jipi5lik357-ocaml4.08.1-mccs-dev.drv
/nix/store/czn6n55lllm64s684cr6d77blrrk5z8c-dose.drv
/nix/store/wvki19p5217y5d2lj38bj7vcjxrqpg3d-ocaml4.08.1-opam-solver-dev.drv
/nix/store/ip9j6m9md6l6j9mj5yq4f948qjfh7sd8-opam2nix-1.1.0.drv
/nix/store/irg7hhssijk6l8l6asszp6s3bka3b73z-opam.drv
/nix/store/wrcjsig8csxhrlvd2q81nmx98y9l99v3-ocaml-config-1.drv
/nix/store/19zmfdih3vc6gal2bw3icbrfr3gms8ki-ocaml-4.08.1.drv
/nix/store/i96pwflzsh76fg81ichcimzksqp103xg-opam.drv
/nix/store/dhgs4mgakpr9vv6lvp6pl5173vchh1l0-base-unix-base.drv
/nix/store/2hzzq6h3469sfvljd3kx018m4nr22cdy-opam.drv
/nix/store/k29wq55qpm1sdihymchwmx21y2kfxrdd-base-threads-base.drv
/nix/store/v7v9vpsk020cmc7zwcrdflm2ic6471yb-opam.drv
/nix/store/5vbxc841ari3g0yf41bgsdrjrpwlh0pj-dune-2.5.1.drv
/nix/store/h80fackh6dayp935ybvgwawixvvxdg4h-opam.drv
/nix/store/3x71rram9zg77g3ryq4cld070y7wvj71-ppx_tools-6.2.drv
/nix/store/jpz408iy778m34l04j1mg64gfxqdfjvf-opam.drv
/nix/store/571ccbb9q4r9fpvj2wvqcfgb235bda32-ppx_derivers-1.2.1.drv
/nix/store/85zsgp9hpgg3q0i9naba6kjcc5a6vbws-v4.5.tar.gz.drv
/nix/store/g7ypdgl777fpxx8aq40kq9pym1jn5hgj-opam.drv
/nix/store/i33naxigrn4yvj1sv9lx716ap0x8wivx-opam.drv
/nix/store/gcbrw62bdqwssp3kgr5nzjrcyjmk8rlz-cppo-1.6.6.drv
/nix/store/plgm3s4xpd53xs5v881a0lpsyqgcg69v-ocaml-migrate-parsetree-v1.7.3.tbz.drv
/nix/store/9yxl9xppawp55qr7sv5650m3gs6nwg63-opam.drv
/nix/store/dff63w1q6m9xh1985dcl4yjpq3758dwn-result-1.5.tbz.drv
/nix/store/wgpx9h0j1lc2i7vyphxw9gbh1dii1903-result-1.5.drv
/nix/store/zjhx9wv4kpshpvccchlb3hcqlzm4zhar-opam.drv
/nix/store/wg8vnf1g4hs7qspihjij6fr8maibjypl-ocaml-migrate-parsetree-1.7.3.drv
/nix/store/pq8kblmzk72w0zb3y5yrv6xkskkm1psc-setupHook.sh.drv
/nix/store/2j5g313afgk01py4bbg1wla5h57msdqs-opam.drv
/nix/store/q3h3q15fl6s7nl5wss0vghj1g8z70ycx-conf-m4-1.drv
/nix/store/xs9mlxwainsw0rf8j1r7p8i94pc2hlx1-opam.drv
/nix/store/35jbvgq6bw2fy0ymrr4f96ahfggzprc9-ocamlfind-1.8.1.drv
/nix/store/hsnnc1pb9dmd2vgz1kqmpz73n580afsw-opam.drv
/nix/store/y08v9arvwzlbzqg1d7jq4ngbvfbkqy3k-ppxfind-1.4.drv
/nix/store/0cy03q96rhxfnrpbmnpg3jzqpmqy0kiq-ppx_deriving-4.5.drv
/nix/store/sx6qfwma18p2gg0bngnfzvazqw38szw8-opam.drv
/nix/store/0ha54cvc03dd3p90p450s7g6dgynp1r9-base-bigarray-base.drv
/nix/store/ff1hh3hi4zb65s0v5fm2924rjf6199im-edukera-archetype.zip.drv
/nix/store/1gij5kxd25bfv5l86rmq6mzcm6ygi5kr-vscode-extension-edukera-archetype-0.34.0.drv
/nix/store/298l7zzis7ykrqhdlxysdb6km67ry7gv-source.drv
/nix/store/k5wqpal1jxicdvz5xrw717bxzp25g6a6-v1.3.tar.gz.drv
/nix/store/lxznwjr1a7hpc9vx7pip56fsr03qmwb1-opam.drv
/nix/store/3ljkplvp1spgipby5krjqmry7661vaa6-num-1.3.drv
/nix/store/l5p9400yzx4acnk2r3x0qaywfrj402q7-vscode-extensions.drv
/nix/store/4nvdir1hgksyp8az26yizsh22b0x3xbg-vscode-with-extensions-1.48.2.drv
/nix/store/pn2pivgpay54zn9xm7hgnvn62ic33hdn-opam.drv
/nix/store/f2m5vlkvwznsd0f83q78hr4lv343k4xa-visitors-20200210.drv
/nix/store/d3vjy9jr76vg8kbycfpmdr2ym15y0sc7-opam.drv
/nix/store/s6v593rjmrskglxslhj7h98kbgcnpwg9-v3.5.3.tar.gz.drv
/nix/store/haw44558xv48am52svchkp85qbsldkch-yojson-1.7.0.tbz.drv
/nix/store/kr4crpz8bcwnbvq9mqaqcpiq744mamkl-easy-format-1.3.2.tbz.drv
/nix/store/zi51b03w5dq1qjl5900zk8lypr3bld2h-opam.drv
/nix/store/hzg9kv5h05wnjb7igm0hdmq47jwr0ray-easy-format-1.3.2.drv
/nix/store/lpqxfn1vp40ji03cl9x1rlbdh7wxgm9d-opam.drv
/nix/store/z7nybrp80al6993fzfvlb84dy567gsrk-opam.drv
/nix/store/snxvfx5qhzrjx1hyjf33kxvxqrzw22pl-biniou-1.2.1.drv
/nix/store/s8xja9l1y7a2jxgy7wnvp867p4d4kz08-yojson-1.7.0.drv
/nix/store/fb18yxww5586qga76s4zl83lcs5wz9xn-ppx_deriving_yojson-3.5.3.drv
/nix/store/cmn8qm42iagnkyqy3mmwgmhqaf270s5s-opam.drv
/nix/store/766jq3ih30swh6fc9qs8x7hqjmzsjl25-opam.drv
/nix/store/h8ylysz070kh3v81m6mh0wrvx3skbq65-menhirLib-20200624.drv
/nix/store/9679a842kd32a742315bj67gc3pkv9cy-opam.drv
/nix/store/rya0mj7549bfkzpl9r2sywrr4n4sialr-menhirSdk-20200624.drv
/nix/store/lzbp2zpqw93nhr2hqar1djy2vffgkzix-menhir-20200624.drv
/nix/store/98r722lg2lw1gw64zpgnrsavm96rpzym-digestif-v0.7.3.tbz.drv
/nix/store/8cwajwjcwxjfnh59gdi1yfwc5k7vs249-opam.drv
/nix/store/qyvd144l1y5qhxrl2zmw78vmcaaix23p-eqaf-0.7.drv
/nix/store/slkdkwv9dbb1bsqq6wypi9p204hj9527-opam.drv
/nix/store/acxj00fahm51w7i0595xggzfh4qz8fdf-opam.drv
/nix/store/w3733pwbkffq119drfjaj9nxl1caf1kf-base-bytes-base.drv
/nix/store/zsxabdraggcap5dsqddbz12li4ar6555-digestif-0.7.3.drv
/nix/store/66ljz3vnvyx2vnl5jpgpss10h67m7f0p-archetype-development.drv
/nix/store/d500kaff383rxxj4iv4wwbi3gxajslwf-ocaml4.10.0-psmt2-frontend-0.2.drv
/nix/store/ir44pja8f678j2a234wqr9s9jm3zxgwi-ocaml4.10.0-ocplib-simplex-0.4.drv
/nix/store/rnwx0mn3zwd4sryr8ygnjap1hks9f5v4-ocaml4.10.0-alt-ergo-lib-2.3.3.drv
/nix/store/b3zw3fqar0bhqqjlms4w4syba0c9p29q-ocaml4.10.0-alt-ergo-parsers-2.3.3.drv
/nix/store/nnykh2agrh8cq5c90dqwwlykl4bmkpf5-why3-1.3.2.tar.gz.drv
/nix/store/bhdxnh1bx2cix4gakd4lzqc56wqqpmqw-why3-1.3.2.drv
/nix/store/caakrmqy90qfh8gaf4k5n90m95v12gq7-cvc3-2.4.1.drv
/nix/store/lgm44196b0rafawlg0haa2dcn7gbn07n-ocaml4.10.0-alt-ergo-2.3.3.drv
building '/nix/store/caakrmqy90qfh8gaf4k5n90m95v12gq7-cvc3-2.4.1.drv'...
unpacking sources
unpacking source archive /nix/store/c5zn7db2wqqibidg43jjz2kr0ix3rrs4-cvc3-2.4.1.tar.gz
source root is cvc3-2.4.1
setting SOURCE_DATE_EPOCH to timestamp 1314919120 of file cvc3-2.4.1/VERSION
patching sources
applying patch /nix/store/8jvmnkq79c6k3zcl4ym9f13czbcz9n1g-cvc3-2.4.1-gccv6-fix.patch
patching file src/expr/expr_value.cpp
patching file src/include/cdmap.h
patching file src/include/expr_hash.h
patching file src/include/expr_value.h
patching file src/theory_core/theory_core.cpp
configuring
sed: couldn't edit .: not a regular file
sed: couldn't edit ./test: not a regular file
sed: couldn't edit ./doc: not a regular file
sed: couldn't edit ./src: not a regular file
sed: couldn't edit ./src/cvc3: not a regular file
sed: couldn't edit ./src/theory_simulate: not a regular file
sed: couldn't edit ./src/context: not a regular file
sed: couldn't edit ./src/theory_records: not a regular file
sed: couldn't edit ./src/theory_arith: not a regular file
sed: couldn't edit ./src/include: not a regular file
sed: couldn't edit ./src/c_interface: not a regular file
sed: couldn't edit ./src/theorem: not a regular file
sed: couldn't edit ./src/translator: not a regular file
sed: couldn't edit ./src/theory_uf: not a regular file
sed: couldn't edit ./src/parser: not a regular file
sed: couldn't edit ./src/search: not a regular file
sed: couldn't edit ./src/theory_core: not a regular file
sed: couldn't edit ./src/theory_array: not a regular file
sed: couldn't edit ./src/theory_bitvector: not a regular file
sed: couldn't edit ./src/theory_quant: not a regular file
sed: couldn't edit ./src/expr: not a regular file
sed: couldn't edit ./src/util: not a regular file
sed: couldn't edit ./src/vcl: not a regular file
sed: couldn't edit ./src/theory_datatype: not a regular file
sed: couldn't edit ./src/sat: not a regular file
sed: couldn't edit ./emacs: not a regular file
sed: couldn't edit ./testc: not a regular file
sed: couldn't edit ./java: not a regular file
sed: couldn't edit ./java/src: not a regular file
sed: couldn't edit ./java/src/cvc3: not a regular file
sed: couldn't edit ./java/include: not a regular file
sed: couldn't edit ./java/include/cvc3: not a regular file
sed: couldn't edit ./bin: not a regular file
configure flags: --disable-static --prefix=/nix/store/sjpdvyzl4x4blh546x5hfmbyz1lad1ff-cvc3-2.4.1
checking whether the C++ compiler works... yes
checking for C++ compiler default output file name... a.out
checking for suffix of executables...
checking whether we are cross compiling... no
checking for suffix of object files... o
checking whether we are using the GNU C++ compiler... yes
checking whether g++ accepts -g... yes
checking how to run the C++ preprocessor... g++ -E
checking for ar... ar
checking build system type... x86_64-unknown-linux-gnu
checking host system type... x86_64-unknown-linux-gnu
checking for install... /nix/store/2f6zzvixj3wsj81flbdcpc6fdscgx4ai-coreutils-8.31/bin/install
checking for ldconfig... /nix/store/r5xqfk8p7c79yqphy25rbvm71yfvrzh4-glibc-2.31-bin/bin/ldconfig
checking for time... not found
configure: WARNING: Regression tests depend upon GNU time.
checking for perl... /nix/store/5b6853g3y2wvzc48l6921a6qcr55lqk2-perl-5.32.0/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)... 9.3.0
checking for gmp... yes
checking vector usability... yes
checking vector presence... yes
checking for vector... yes
checking list usability... yes
checking list presence... yes
checking for list... yes
checking deque usability... yes
checking deque presence... yes
checking for deque... yes
checking set usability... yes
checking set presence... yes
checking for set... yes
checking string usability... yes
checking string presence... yes
checking for string... yes
checking cstdlib usability... yes
checking cstdlib presence... yes
checking for cstdlib... yes
checking cstdio usability... yes
checking cstdio presence... yes
checking for cstdio... yes
checking functional usability... yes
checking functional presence... yes
checking for functional... yes
checking algorithm usability... yes
checking algorithm presence... yes
checking for algorithm... yes
checking for doxygen... no
checking for doxytag... no
checking for fig2dev... no
checking for dot... NO
checking for etags... no
checking for ebrowse... no
configure: creating ./config.status
config.status: creating Makefile.local
config.status: creating LICENSE
config.status: creating src/cvc3.pc
config.status: creating bin/unpack
config.status: creating bin/run_tests
config.status: creating bin/cvc2smt
config.status: creating doc/Doxyfile
config.status: creating doc/Makefile
CVC3 is configured successfully.
Platform: x86_64-linux-gnu
Version: 2.4.1
Computer arithmetic: GMP
Run ./configure --help for additional configuration options.
Type 'make' to compile CVC3.
*** 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
building
build flags: SHELL=/nix/store/6ffp6xbr6j2ryqw2dafbbvv55ggq16iv-bash-4.4-p23/bin/bash
cd /build/cvc3-2.4.1/src; make VERSION=2.4.1
make[1]: Entering directory '/build/cvc3-2.4.1/src'
cd util && make
make[2]: Entering directory '/build/cvc3-2.4.1/src/util'
Making dependencies for debug.cpp statistics.cpp rational.cpp rational-native.cpp rational-gmp.cpp
g++ -M -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DRATIONAL_GMP debug.cpp statistics.cpp rational.cpp rational-native.cpp rational-gmp.cpp >> /build/cvc3-2.4.1/obj/util/x86_64-linux-gnu/Makefile.tmp
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DRATIONAL_GMP -c debug.cpp -o '/build/cvc3-2.4.1/obj/util/x86_64-linux-gnu/debug.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DRATIONAL_GMP -c statistics.cpp -o '/build/cvc3-2.4.1/obj/util/x86_64-linux-gnu/statistics.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DRATIONAL_GMP -c rational.cpp -o '/build/cvc3-2.4.1/obj/util/x86_64-linux-gnu/rational.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DRATIONAL_GMP -c rational-native.cpp -o '/build/cvc3-2.4.1/obj/util/x86_64-linux-gnu/rational-native.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DRATIONAL_GMP -c rational-gmp.cpp -o '/build/cvc3-2.4.1/obj/util/x86_64-linux-gnu/rational-gmp.o'
ar ruvs '/build/cvc3-2.4.1/lib/x86_64-linux-gnu/libcvc_util.a' /build/cvc3-2.4.1/obj/util/x86_64-linux-gnu/debug.o /build/cvc3-2.4.1/obj/util/x86_64-linux-gnu/statistics.o /build/cvc3-2.4.1/obj/util/x86_64-linux-gnu/rational.o /build/cvc3-2.4.1/obj/util/x86_64-linux-gnu/rational-native.o /build/cvc3-2.4.1/obj/util/x86_64-linux-gnu/rational-gmp.o
ar: `u' modifier ignored since `D' is the default (see `U')
ar: creating /build/cvc3-2.4.1/lib/x86_64-linux-gnu/libcvc_util.a
a - /build/cvc3-2.4.1/obj/util/x86_64-linux-gnu/debug.o
a - /build/cvc3-2.4.1/obj/util/x86_64-linux-gnu/statistics.o
a - /build/cvc3-2.4.1/obj/util/x86_64-linux-gnu/rational.o
a - /build/cvc3-2.4.1/obj/util/x86_64-linux-gnu/rational-native.o
a - /build/cvc3-2.4.1/obj/util/x86_64-linux-gnu/rational-gmp.o
make[2]: Leaving directory '/build/cvc3-2.4.1/src/util'
cd context && make
make[2]: Entering directory '/build/cvc3-2.4.1/src/context'
Making dependencies for context.cpp cdflags.cpp
g++ -M -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include context.cpp cdflags.cpp >> /build/cvc3-2.4.1/obj/context/x86_64-linux-gnu/Makefile.tmp
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c context.cpp -o '/build/cvc3-2.4.1/obj/context/x86_64-linux-gnu/context.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c cdflags.cpp -o '/build/cvc3-2.4.1/obj/context/x86_64-linux-gnu/cdflags.o'
ar ruvs '/build/cvc3-2.4.1/lib/x86_64-linux-gnu/libcontext.a' /build/cvc3-2.4.1/obj/context/x86_64-linux-gnu/context.o /build/cvc3-2.4.1/obj/context/x86_64-linux-gnu/cdflags.o
ar: `u' modifier ignored since `D' is the default (see `U')
ar: creating /build/cvc3-2.4.1/lib/x86_64-linux-gnu/libcontext.a
a - /build/cvc3-2.4.1/obj/context/x86_64-linux-gnu/context.o
a - /build/cvc3-2.4.1/obj/context/x86_64-linux-gnu/cdflags.o
make[2]: Leaving directory '/build/cvc3-2.4.1/src/context'
cd expr && make
make[2]: Entering directory '/build/cvc3-2.4.1/src/expr'
Making dependencies for expr.cpp expr_manager.cpp expr_stream.cpp expr_value.cpp expr_op.cpp
g++ -M -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include expr.cpp expr_manager.cpp expr_stream.cpp expr_value.cpp expr_op.cpp >> /build/cvc3-2.4.1/obj/expr/x86_64-linux-gnu/Makefile.tmp
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c expr.cpp -o '/build/cvc3-2.4.1/obj/expr/x86_64-linux-gnu/expr.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c expr_manager.cpp -o '/build/cvc3-2.4.1/obj/expr/x86_64-linux-gnu/expr_manager.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c expr_stream.cpp -o '/build/cvc3-2.4.1/obj/expr/x86_64-linux-gnu/expr_stream.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c expr_value.cpp -o '/build/cvc3-2.4.1/obj/expr/x86_64-linux-gnu/expr_value.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c expr_op.cpp -o '/build/cvc3-2.4.1/obj/expr/x86_64-linux-gnu/expr_op.o'
ar ruvs '/build/cvc3-2.4.1/lib/x86_64-linux-gnu/libexpr.a' /build/cvc3-2.4.1/obj/expr/x86_64-linux-gnu/expr.o /build/cvc3-2.4.1/obj/expr/x86_64-linux-gnu/expr_manager.o /build/cvc3-2.4.1/obj/expr/x86_64-linux-gnu/expr_stream.o /build/cvc3-2.4.1/obj/expr/x86_64-linux-gnu/expr_value.o /build/cvc3-2.4.1/obj/expr/x86_64-linux-gnu/expr_op.o
ar: `u' modifier ignored since `D' is the default (see `U')
ar: creating /build/cvc3-2.4.1/lib/x86_64-linux-gnu/libexpr.a
a - /build/cvc3-2.4.1/obj/expr/x86_64-linux-gnu/expr.o
a - /build/cvc3-2.4.1/obj/expr/x86_64-linux-gnu/expr_manager.o
a - /build/cvc3-2.4.1/obj/expr/x86_64-linux-gnu/expr_stream.o
a - /build/cvc3-2.4.1/obj/expr/x86_64-linux-gnu/expr_value.o
a - /build/cvc3-2.4.1/obj/expr/x86_64-linux-gnu/expr_op.o
make[2]: Leaving directory '/build/cvc3-2.4.1/src/expr'
cd theorem && make
make[2]: Entering directory '/build/cvc3-2.4.1/src/theorem'
Making dependencies for assumptions.cpp theorem.cpp theorem_manager.cpp theorem_producer.cpp common_theorem_producer.cpp
g++ -M -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include assumptions.cpp theorem.cpp theorem_manager.cpp theorem_producer.cpp common_theorem_producer.cpp >> /build/cvc3-2.4.1/obj/theorem/x86_64-linux-gnu/Makefile.tmp
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c assumptions.cpp -o '/build/cvc3-2.4.1/obj/theorem/x86_64-linux-gnu/assumptions.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c theorem.cpp -o '/build/cvc3-2.4.1/obj/theorem/x86_64-linux-gnu/theorem.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c theorem_manager.cpp -o '/build/cvc3-2.4.1/obj/theorem/x86_64-linux-gnu/theorem_manager.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c theorem_producer.cpp -o '/build/cvc3-2.4.1/obj/theorem/x86_64-linux-gnu/theorem_producer.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c common_theorem_producer.cpp -o '/build/cvc3-2.4.1/obj/theorem/x86_64-linux-gnu/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]
565 | CHECK_SOUND(!e.getExpr() == not_e.getExpr(),
| ^~
/build/cvc3-2.4.1/src/include/theorem_producer.h:83:39: note: in definition of macro 'CHECK_SOUND'
83 | #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
565 | CHECK_SOUND(!e.getExpr() == not_e.getExpr(),
| ^~~~~~~~~~~~
/build/cvc3-2.4.1/src/include/theorem_producer.h:83:39: note: in definition of macro 'CHECK_SOUND'
83 | #define CHECK_SOUND(cond, msg) { if(!(cond)) \
| ^~~~
ar ruvs '/build/cvc3-2.4.1/lib/x86_64-linux-gnu/libtheorem.a' /build/cvc3-2.4.1/obj/theorem/x86_64-linux-gnu/assumptions.o /build/cvc3-2.4.1/obj/theorem/x86_64-linux-gnu/theorem.o /build/cvc3-2.4.1/obj/theorem/x86_64-linux-gnu/theorem_manager.o /build/cvc3-2.4.1/obj/theorem/x86_64-linux-gnu/theorem_producer.o /build/cvc3-2.4.1/obj/theorem/x86_64-linux-gnu/common_theorem_producer.o
ar: `u' modifier ignored since `D' is the default (see `U')
ar: creating /build/cvc3-2.4.1/lib/x86_64-linux-gnu/libtheorem.a
a - /build/cvc3-2.4.1/obj/theorem/x86_64-linux-gnu/assumptions.o
a - /build/cvc3-2.4.1/obj/theorem/x86_64-linux-gnu/theorem.o
a - /build/cvc3-2.4.1/obj/theorem/x86_64-linux-gnu/theorem_manager.o
a - /build/cvc3-2.4.1/obj/theorem/x86_64-linux-gnu/theorem_producer.o
a - /build/cvc3-2.4.1/obj/theorem/x86_64-linux-gnu/common_theorem_producer.o
make[2]: Leaving directory '/build/cvc3-2.4.1/src/theorem'
cd sat && make
make[2]: Entering directory '/build/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 -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DDPLL_BASIC 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 >> /build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/Makefile.tmp
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DDPLL_BASIC -c xchaff.cpp -o '/build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/xchaff.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]
48 | 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'
48 | if (var.id != _solver->num_variables()) v.id = var.id+1; return v; }
| ^~~~~~
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DDPLL_BASIC -c xchaff_dbase.cpp -o '/build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/xchaff_dbase.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DDPLL_BASIC -c xchaff_solver.cpp -o '/build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/xchaff_solver.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DDPLL_BASIC -c xchaff_utils.cpp -o '/build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/xchaff_utils.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DDPLL_BASIC -c cnf.cpp -o '/build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/cnf.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DDPLL_BASIC -c cnf_manager.cpp -o '/build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/cnf_manager.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DDPLL_BASIC -c cnf_theorem_producer.cpp -o '/build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/cnf_theorem_producer.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DDPLL_BASIC -c dpllt_basic.cpp -o '/build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/dpllt_basic.o'
dpllt_basic.cpp: In member function 'void SAT::DPLLTBasic::handle_result(SatSolver::SATStatus)':
dpllt_basic.cpp:172:16: warning: variable 'result' set but not used [-Wunused-but-set-variable]
172 | const char * result = "UNKNOWN";
| ^~~~~~
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DDPLL_BASIC -c sat_api.cpp -o '/build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/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]
29 | 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'
32 | os << "Number of Clauses\t\t\t" << NumClauses() << endl;
| ^~
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DDPLL_BASIC -c dpllt_minisat.cpp -o '/build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/dpllt_minisat.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DDPLL_BASIC -c minisat_types.cpp -o '/build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/minisat_types.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DDPLL_BASIC -c minisat_derivation.cpp -o '/build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/minisat_derivation.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DDPLL_BASIC -c minisat_solver.cpp -o '/build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/minisat_solver.o'
ar ruvs '/build/cvc3-2.4.1/lib/x86_64-linux-gnu/libsat.a' /build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/xchaff.o /build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/xchaff_dbase.o /build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/xchaff_solver.o /build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/xchaff_utils.o /build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/cnf.o /build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/cnf_manager.o /build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/cnf_theorem_producer.o /build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/dpllt_basic.o /build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/sat_api.o /build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/dpllt_minisat.o /build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/minisat_types.o /build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/minisat_derivation.o /build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/minisat_solver.o
ar: `u' modifier ignored since `D' is the default (see `U')
ar: creating /build/cvc3-2.4.1/lib/x86_64-linux-gnu/libsat.a
a - /build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/xchaff.o
a - /build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/xchaff_dbase.o
a - /build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/xchaff_solver.o
a - /build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/xchaff_utils.o
a - /build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/cnf.o
a - /build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/cnf_manager.o
a - /build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/cnf_theorem_producer.o
a - /build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/dpllt_basic.o
a - /build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/sat_api.o
a - /build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/dpllt_minisat.o
a - /build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/minisat_types.o
a - /build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/minisat_derivation.o
a - /build/cvc3-2.4.1/obj/sat/x86_64-linux-gnu/minisat_solver.o
make[2]: Leaving directory '/build/cvc3-2.4.1/src/sat'
cd theory_core && make
make[2]: Entering directory '/build/cvc3-2.4.1/src/theory_core'
Making dependencies for theory.cpp theory_core.cpp core_theorem_producer.cpp expr_transform.cpp bryant.cpp
g++ -M -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include theory.cpp theory_core.cpp core_theorem_producer.cpp expr_transform.cpp bryant.cpp >> /build/cvc3-2.4.1/obj/theory_core/x86_64-linux-gnu/Makefile.tmp
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c theory.cpp -o '/build/cvc3-2.4.1/obj/theory_core/x86_64-linux-gnu/theory.o'
In file included from /build/cvc3-2.4.1/src/include/expr_stream.h:36,
from /build/cvc3-2.4.1/src/include/theory.h:25,
from /build/cvc3-2.4.1/src/include/theory_core.h:25,
from theory.cpp:22:
/build/cvc3-2.4.1/src/include/expr.h: In member function 'CVC3::Theory* CVC3::Theory::theoryOf(const CVC3::Expr&)':
/build/cvc3-2.4.1/src/include/expr.h:1017:17: warning: '<anonymous>' may be used uninitialized in this function [-Wmaybe-uninitialized]
1017 | return getKind() == APPLY; }
| ~~~~~~~^~
/build/cvc3-2.4.1/src/include/expr.h: In member function 'CVC3::Theory* CVC3::Theory::theoryOf(const CVC3::Type&)':
/build/cvc3-2.4.1/src/include/expr.h:1017:17: warning: '<anonymous>' is used uninitialized in this function [-Wuninitialized]
1017 | return getKind() == APPLY; }
| ~~~~~~~^~
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c theory_core.cpp -o '/build/cvc3-2.4.1/obj/theory_core/x86_64-linux-gnu/theory_core.o'
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]
3419 | 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'
3421 | if(inconsistent()) {
| ^~
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c core_theorem_producer.cpp -o '/build/cvc3-2.4.1/obj/theory_core/x86_64-linux-gnu/core_theorem_producer.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c expr_transform.cpp -o '/build/cvc3-2.4.1/obj/theory_core/x86_64-linux-gnu/expr_transform.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c bryant.cpp -o '/build/cvc3-2.4.1/obj/theory_core/x86_64-linux-gnu/bryant.o'
bryant.cpp: In member function 'void CVC3::ExprTransform::GetPEqs(const CVC3::Expr&, CVC3::ExprTransform::B_name_map&, std::set<CVC3::Expr>&, std::set<CVC3::Expr>&, CVC3::ExprTransform::T_generator_map&, std::set<CVC3::Expr>&)':
bryant.cpp:402:5: warning: this 'if' clause does not guard... [-Wmisleading-indentation]
402 | 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'
404 | if (e.isEq()) {
| ^~
bryant.cpp: In member function 'CVC3::Expr CVC3::ExprTransform::ConstrainedConstraints(std::set<CVC3::Expr>&, CVC3::ExprTransform::T_generator_map&, CVC3::ExprTransform::B_name_map&, CVC3::ExprTransform::B_Term_map&, std::set<CVC3::Expr>&, std::set<CVC3::Expr>&, std::set<CVC3::Expr>&)':
bryant.cpp:452:3: warning: this 'else' clause does not guard... [-Wmisleading-indentation]
452 | else
| ^~~~
bryant.cpp:454:4: note: ...this statement, but the latter is misleadingly indented as if it were guarded by the 'else'
454 | for (set<Expr>::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]
470 | if (!Value == Temp)
| ^~
bryant.cpp:470:10: note: add parentheses around left hand side expression to silence this warning
470 | if (!Value == Temp)
| ^~~~~~
| ( )
ar ruvs '/build/cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_core.a' /build/cvc3-2.4.1/obj/theory_core/x86_64-linux-gnu/theory.o /build/cvc3-2.4.1/obj/theory_core/x86_64-linux-gnu/theory_core.o /build/cvc3-2.4.1/obj/theory_core/x86_64-linux-gnu/core_theorem_producer.o /build/cvc3-2.4.1/obj/theory_core/x86_64-linux-gnu/expr_transform.o /build/cvc3-2.4.1/obj/theory_core/x86_64-linux-gnu/bryant.o
ar: `u' modifier ignored since `D' is the default (see `U')
ar: creating /build/cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_core.a
a - /build/cvc3-2.4.1/obj/theory_core/x86_64-linux-gnu/theory.o
a - /build/cvc3-2.4.1/obj/theory_core/x86_64-linux-gnu/theory_core.o
a - /build/cvc3-2.4.1/obj/theory_core/x86_64-linux-gnu/core_theorem_producer.o
a - /build/cvc3-2.4.1/obj/theory_core/x86_64-linux-gnu/expr_transform.o
a - /build/cvc3-2.4.1/obj/theory_core/x86_64-linux-gnu/bryant.o
make[2]: Leaving directory '/build/cvc3-2.4.1/src/theory_core'
cd theory_arith && make
make[2]: Entering directory '/build/cvc3-2.4.1/src/theory_arith'
Making dependencies for arith_theorem_producer_old.cpp arith_theorem_producer.cpp arith_theorem_producer3.cpp theory_arith.cpp theory_arith_old.cpp theory_arith_new.cpp theory_arith3.cpp
g++ -M -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include arith_theorem_producer_old.cpp arith_theorem_producer.cpp arith_theorem_producer3.cpp theory_arith.cpp theory_arith_old.cpp theory_arith_new.cpp theory_arith3.cpp >> /build/cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/Makefile.tmp
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c arith_theorem_producer_old.cpp -o '/build/cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer_old.o'
arith_theorem_producer_old.cpp: In member function 'virtual CVC3::Theorem CVC3::ArithTheoremProducerOld::canonMult(const CVC3::Expr&)':
arith_theorem_producer_old.cpp:797:50: warning: logical not is only applied to the left hand side of comparison [-Wlogical-not-parentheses]
797 | 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
797 | if (count_non_trivial > 0 && !count_constants == (e.arity() - 1)) {
| ^~~~~~~~~~~~~~~~
| ( )
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c arith_theorem_producer.cpp -o '/build/cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c arith_theorem_producer3.cpp -o '/build/cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer3.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c theory_arith.cpp -o '/build/cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/theory_arith.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c theory_arith_old.cpp -o '/build/cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/theory_arith_old.o'
theory_arith_old.cpp: In member function 'bool CVC3::TheoryArithOld::findBounds(const CVC3::Expr&, CVC3::Rational&, CVC3::Rational&)':
theory_arith_old.cpp:2782:24: warning: variable 'strictUB' set but not used [-Wunused-but-set-variable]
2782 | bool strictLB=false, strictUB=false;
| ^~~~~~~~
theory_arith_old.cpp: In member function 'int CVC3::TheoryArithOld::computeTermBounds()':
theory_arith_old.cpp:5565:42: warning: enum constant in boolean context [-Wint-in-bool-context]
5565 | if (!isConstrained(v, QueryWithCacheAll)) {
| ^
theory_arith_old.cpp:5568:62: warning: enum constant in boolean context [-Wint-in-bool-context]
5568 | bool constrainedAbove = isConstrained(v, QueryWithCacheAll);
| ^
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c theory_arith_new.cpp -o '/build/cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/theory_arith_new.o'
theory_arith_new.cpp: In member function 'bool CVC3::TheoryArithNew::findBounds(const CVC3::Expr&, CVC3::Rational&, CVC3::Rational&)':
theory_arith_new.cpp:1350:24: warning: variable 'strictUB' set but not used [-Wunused-but-set-variable]
1350 | bool strictLB=false, strictUB=false;
| ^~~~~~~~
theory_arith_new.cpp: In member function 'std::string CVC3::TheoryArithNew::tableauxAsString() const':
theory_arith_new.cpp:3350:30: warning: variable 'row_end' set but not used [-Wunused-but-set-variable]
3350 | TebleauxMap::const_iterator row_end = tableaux.end();
| ^~~~~~~
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c theory_arith3.cpp -o '/build/cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/theory_arith3.o'
theory_arith3.cpp: In member function 'bool CVC3::TheoryArith3::findBounds(const CVC3::Expr&, CVC3::Rational&, CVC3::Rational&)':
theory_arith3.cpp:2199:24: warning: variable 'strictUB' set but not used [-Wunused-but-set-variable]
2199 | bool strictLB=false, strictUB=false;
| ^~~~~~~~
ar ruvs '/build/cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_arith.a' /build/cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer_old.o /build/cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer.o /build/cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer3.o /build/cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/theory_arith.o /build/cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/theory_arith_old.o /build/cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/theory_arith_new.o /build/cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/theory_arith3.o
ar: `u' modifier ignored since `D' is the default (see `U')
ar: creating /build/cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_arith.a
a - /build/cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer_old.o
a - /build/cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer.o
a - /build/cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer3.o
a - /build/cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/theory_arith.o
a - /build/cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/theory_arith_old.o
a - /build/cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/theory_arith_new.o
a - /build/cvc3-2.4.1/obj/theory_arith/x86_64-linux-gnu/theory_arith3.o
make[2]: Leaving directory '/build/cvc3-2.4.1/src/theory_arith'
cd theory_array && make
make[2]: Entering directory '/build/cvc3-2.4.1/src/theory_array'
Making dependencies for array_theorem_producer.cpp theory_array.cpp
g++ -M -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include array_theorem_producer.cpp theory_array.cpp >> /build/cvc3-2.4.1/obj/theory_array/x86_64-linux-gnu/Makefile.tmp
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c array_theorem_producer.cpp -o '/build/cvc3-2.4.1/obj/theory_array/x86_64-linux-gnu/array_theorem_producer.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c theory_array.cpp -o '/build/cvc3-2.4.1/obj/theory_array/x86_64-linux-gnu/theory_array.o'
ar ruvs '/build/cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_array.a' /build/cvc3-2.4.1/obj/theory_array/x86_64-linux-gnu/array_theorem_producer.o /build/cvc3-2.4.1/obj/theory_array/x86_64-linux-gnu/theory_array.o
ar: `u' modifier ignored since `D' is the default (see `U')
ar: creating /build/cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_array.a
a - /build/cvc3-2.4.1/obj/theory_array/x86_64-linux-gnu/array_theorem_producer.o
a - /build/cvc3-2.4.1/obj/theory_array/x86_64-linux-gnu/theory_array.o
make[2]: Leaving directory '/build/cvc3-2.4.1/src/theory_array'
cd theory_bitvector && make
make[2]: Entering directory '/build/cvc3-2.4.1/src/theory_bitvector'
Making dependencies for bitvector_theorem_producer.cpp theory_bitvector.cpp
g++ -M -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include bitvector_theorem_producer.cpp theory_bitvector.cpp >> /build/cvc3-2.4.1/obj/theory_bitvector/x86_64-linux-gnu/Makefile.tmp
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c bitvector_theorem_producer.cpp -o '/build/cvc3-2.4.1/obj/theory_bitvector/x86_64-linux-gnu/bitvector_theorem_producer.o'
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]
2996 | vector<Expr>::iterator jend = flattenkids.end();
| ^~~~
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c theory_bitvector.cpp -o '/build/cvc3-2.4.1/obj/theory_bitvector/x86_64-linux-gnu/theory_bitvector.o'
theory_bitvector.cpp: In member function 'CVC3::Theorem CVC3::TheoryBitvector::rewriteBV(const CVC3::Expr&, CVC3::ExprMap<CVC3::Theorem>&, int)':
theory_bitvector.cpp:1063:11: warning: variable 'hi' set but not used [-Wunused-but-set-variable]
1063 | int hi(-1), low(-1);
| ^~
ar ruvs '/build/cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_bitvector.a' /build/cvc3-2.4.1/obj/theory_bitvector/x86_64-linux-gnu/bitvector_theorem_producer.o /build/cvc3-2.4.1/obj/theory_bitvector/x86_64-linux-gnu/theory_bitvector.o
ar: `u' modifier ignored since `D' is the default (see `U')
ar: creating /build/cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_bitvector.a
a - /build/cvc3-2.4.1/obj/theory_bitvector/x86_64-linux-gnu/bitvector_theorem_producer.o
a - /build/cvc3-2.4.1/obj/theory_bitvector/x86_64-linux-gnu/theory_bitvector.o
make[2]: Leaving directory '/build/cvc3-2.4.1/src/theory_bitvector'
cd theory_datatype && make
make[2]: Entering directory '/build/cvc3-2.4.1/src/theory_datatype'
Making dependencies for datatype_theorem_producer.cpp theory_datatype.cpp theory_datatype_lazy.cpp
g++ -M -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include datatype_theorem_producer.cpp theory_datatype.cpp theory_datatype_lazy.cpp >> /build/cvc3-2.4.1/obj/theory_datatype/x86_64-linux-gnu/Makefile.tmp
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c datatype_theorem_producer.cpp -o '/build/cvc3-2.4.1/obj/theory_datatype/x86_64-linux-gnu/datatype_theorem_producer.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c theory_datatype.cpp -o '/build/cvc3-2.4.1/obj/theory_datatype/x86_64-linux-gnu/theory_datatype.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c theory_datatype_lazy.cpp -o '/build/cvc3-2.4.1/obj/theory_datatype/x86_64-linux-gnu/theory_datatype_lazy.o'
ar ruvs '/build/cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_datatype.a' /build/cvc3-2.4.1/obj/theory_datatype/x86_64-linux-gnu/datatype_theorem_producer.o /build/cvc3-2.4.1/obj/theory_datatype/x86_64-linux-gnu/theory_datatype.o /build/cvc3-2.4.1/obj/theory_datatype/x86_64-linux-gnu/theory_datatype_lazy.o
ar: `u' modifier ignored since `D' is the default (see `U')
ar: creating /build/cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_datatype.a
a - /build/cvc3-2.4.1/obj/theory_datatype/x86_64-linux-gnu/datatype_theorem_producer.o
a - /build/cvc3-2.4.1/obj/theory_datatype/x86_64-linux-gnu/theory_datatype.o
a - /build/cvc3-2.4.1/obj/theory_datatype/x86_64-linux-gnu/theory_datatype_lazy.o
make[2]: Leaving directory '/build/cvc3-2.4.1/src/theory_datatype'
cd theory_quant && make
make[2]: Entering directory '/build/cvc3-2.4.1/src/theory_quant'
Making dependencies for theory_quant.cpp quant_theorem_producer.cpp
g++ -M -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include theory_quant.cpp quant_theorem_producer.cpp >> /build/cvc3-2.4.1/obj/theory_quant/x86_64-linux-gnu/Makefile.tmp
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c theory_quant.cpp -o '/build/cvc3-2.4.1/obj/theory_quant/x86_64-linux-gnu/theory_quant.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=]
9077 | catch (Exception e){
| ^
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c quant_theorem_producer.cpp -o '/build/cvc3-2.4.1/obj/theory_quant/x86_64-linux-gnu/quant_theorem_producer.o'
ar ruvs '/build/cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_quant.a' /build/cvc3-2.4.1/obj/theory_quant/x86_64-linux-gnu/theory_quant.o /build/cvc3-2.4.1/obj/theory_quant/x86_64-linux-gnu/quant_theorem_producer.o
ar: `u' modifier ignored since `D' is the default (see `U')
ar: creating /build/cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_quant.a
a - /build/cvc3-2.4.1/obj/theory_quant/x86_64-linux-gnu/theory_quant.o
a - /build/cvc3-2.4.1/obj/theory_quant/x86_64-linux-gnu/quant_theorem_producer.o
make[2]: Leaving directory '/build/cvc3-2.4.1/src/theory_quant'
cd theory_records && make
make[2]: Entering directory '/build/cvc3-2.4.1/src/theory_records'
Making dependencies for theory_records.cpp records_theorem_producer.cpp
g++ -M -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include theory_records.cpp records_theorem_producer.cpp >> /build/cvc3-2.4.1/obj/theory_records/x86_64-linux-gnu/Makefile.tmp
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c theory_records.cpp -o '/build/cvc3-2.4.1/obj/theory_records/x86_64-linux-gnu/theory_records.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c records_theorem_producer.cpp -o '/build/cvc3-2.4.1/obj/theory_records/x86_64-linux-gnu/records_theorem_producer.o'
ar ruvs '/build/cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_records.a' /build/cvc3-2.4.1/obj/theory_records/x86_64-linux-gnu/theory_records.o /build/cvc3-2.4.1/obj/theory_records/x86_64-linux-gnu/records_theorem_producer.o
ar: `u' modifier ignored since `D' is the default (see `U')
ar: creating /build/cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_records.a
a - /build/cvc3-2.4.1/obj/theory_records/x86_64-linux-gnu/theory_records.o
a - /build/cvc3-2.4.1/obj/theory_records/x86_64-linux-gnu/records_theorem_producer.o
make[2]: Leaving directory '/build/cvc3-2.4.1/src/theory_records'
cd theory_simulate && make
make[2]: Entering directory '/build/cvc3-2.4.1/src/theory_simulate'
Making dependencies for theory_simulate.cpp simulate_theorem_producer.cpp
g++ -M -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include theory_simulate.cpp simulate_theorem_producer.cpp >> /build/cvc3-2.4.1/obj/theory_simulate/x86_64-linux-gnu/Makefile.tmp
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c theory_simulate.cpp -o '/build/cvc3-2.4.1/obj/theory_simulate/x86_64-linux-gnu/theory_simulate.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c simulate_theorem_producer.cpp -o '/build/cvc3-2.4.1/obj/theory_simulate/x86_64-linux-gnu/simulate_theorem_producer.o'
ar ruvs '/build/cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_simulate.a' /build/cvc3-2.4.1/obj/theory_simulate/x86_64-linux-gnu/theory_simulate.o /build/cvc3-2.4.1/obj/theory_simulate/x86_64-linux-gnu/simulate_theorem_producer.o
ar: `u' modifier ignored since `D' is the default (see `U')
ar: creating /build/cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_simulate.a
a - /build/cvc3-2.4.1/obj/theory_simulate/x86_64-linux-gnu/theory_simulate.o
a - /build/cvc3-2.4.1/obj/theory_simulate/x86_64-linux-gnu/simulate_theorem_producer.o
make[2]: Leaving directory '/build/cvc3-2.4.1/src/theory_simulate'
cd theory_uf && make
make[2]: Entering directory '/build/cvc3-2.4.1/src/theory_uf'
Making dependencies for uf_theorem_producer.cpp theory_uf.cpp
g++ -M -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include uf_theorem_producer.cpp theory_uf.cpp >> /build/cvc3-2.4.1/obj/theory_uf/x86_64-linux-gnu/Makefile.tmp
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c uf_theorem_producer.cpp -o '/build/cvc3-2.4.1/obj/theory_uf/x86_64-linux-gnu/uf_theorem_producer.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -c theory_uf.cpp -o '/build/cvc3-2.4.1/obj/theory_uf/x86_64-linux-gnu/theory_uf.o'
ar ruvs '/build/cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_uf.a' /build/cvc3-2.4.1/obj/theory_uf/x86_64-linux-gnu/uf_theorem_producer.o /build/cvc3-2.4.1/obj/theory_uf/x86_64-linux-gnu/theory_uf.o
ar: `u' modifier ignored since `D' is the default (see `U')
ar: creating /build/cvc3-2.4.1/lib/x86_64-linux-gnu/libtheory_uf.a
a - /build/cvc3-2.4.1/obj/theory_uf/x86_64-linux-gnu/uf_theorem_producer.o
a - /build/cvc3-2.4.1/obj/theory_uf/x86_64-linux-gnu/theory_uf.o
make[2]: Leaving directory '/build/cvc3-2.4.1/src/theory_uf'
cd search && make
make[2]: Entering directory '/build/cvc3-2.4.1/src/search'
Making dependencies for clause.cpp search_impl_base.cpp search.cpp search_fast.cpp search_theorem_producer.cpp search_sat.cpp search_simple.cpp variable.cpp circuit.cpp decision_engine.cpp decision_engine_dfs.cpp LFSCObject.cpp LFSCUtilProof.cpp LFSCBoolProof.cpp LFSCConvert.cpp LFSCLraProof.cpp LFSCPrinter.cpp LFSCProof.cpp TReturn.cpp Util.cpp
g++ -M -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DDPLL_BASIC 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 >> /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/Makefile.tmp
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DDPLL_BASIC -c clause.cpp -o '/build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/clause.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DDPLL_BASIC -c search_impl_base.cpp -o '/build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/search_impl_base.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DDPLL_BASIC -c search.cpp -o '/build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/search.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DDPLL_BASIC -c search_fast.cpp -o '/build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/search_fast.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DDPLL_BASIC -c search_theorem_producer.cpp -o '/build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/search_theorem_producer.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DDPLL_BASIC -c search_sat.cpp -o '/build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/search_sat.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DDPLL_BASIC -c search_simple.cpp -o '/build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/search_simple.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DDPLL_BASIC -c variable.cpp -o '/build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/variable.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DDPLL_BASIC -c circuit.cpp -o '/build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/circuit.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DDPLL_BASIC -c decision_engine.cpp -o '/build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/decision_engine.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DDPLL_BASIC -c decision_engine_dfs.cpp -o '/build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/decision_engine_dfs.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DDPLL_BASIC -c LFSCObject.cpp -o '/build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCObject.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DDPLL_BASIC -c LFSCUtilProof.cpp -o '/build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCUtilProof.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DDPLL_BASIC -c LFSCBoolProof.cpp -o '/build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCBoolProof.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DDPLL_BASIC -c LFSCConvert.cpp -o '/build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCConvert.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DDPLL_BASIC -c LFSCLraProof.cpp -o '/build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCLraProof.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DDPLL_BASIC -c LFSCPrinter.cpp -o '/build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCPrinter.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DDPLL_BASIC -c LFSCProof.cpp -o '/build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCProof.o'
LFSCProof.cpp: In member function 'virtual int LFSCProof::checkOp()':
LFSCProof.cpp:91:11: warning: unused variable 'o' [-Wunused-variable]
91 | 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]
193 | int m2 = queryM( ec[1] );
| ^~
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DDPLL_BASIC -c TReturn.cpp -o '/build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/TReturn.o'
TReturn.cpp: In static member function 'static int TReturn::normalize_tr(const CVC3::Expr&, TReturn*&, int, bool, bool)':
TReturn.cpp:127:12: warning: unused variable 'torig' [-Wunused-variable]
127 | TReturn* torig = t1;
| ^~~~~
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -DDPLL_BASIC -c Util.cpp -o '/build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/Util.o'
ar ruvs '/build/cvc3-2.4.1/lib/x86_64-linux-gnu/libsearch.a' /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/clause.o /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/search_impl_base.o /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/search.o /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/search_fast.o /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/search_theorem_producer.o /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/search_sat.o /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/search_simple.o /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/variable.o /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/circuit.o /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/decision_engine.o /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/decision_engine_dfs.o /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCObject.o /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCUtilProof.o /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCBoolProof.o /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCConvert.o /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCLraProof.o /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCPrinter.o /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCProof.o /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/TReturn.o /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/Util.o
ar: `u' modifier ignored since `D' is the default (see `U')
ar: creating /build/cvc3-2.4.1/lib/x86_64-linux-gnu/libsearch.a
a - /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/clause.o
a - /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/search_impl_base.o
a - /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/search.o
a - /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/search_fast.o
a - /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/search_theorem_producer.o
a - /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/search_sat.o
a - /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/search_simple.o
a - /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/variable.o
a - /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/circuit.o
a - /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/decision_engine.o
a - /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/decision_engine_dfs.o
a - /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCObject.o
a - /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCUtilProof.o
a - /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCBoolProof.o
a - /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCConvert.o
a - /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCLraProof.o
a - /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCPrinter.o
a - /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/LFSCProof.o
a - /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/TReturn.o
a - /build/cvc3-2.4.1/obj/search/x86_64-linux-gnu/Util.o
make[2]: Leaving directory '/build/cvc3-2.4.1/src/search'
cd parser && make
make[2]: Entering directory '/build/cvc3-2.4.1/src/parser'
bison -d -y -o parsePL.cpp -p PL --debug -v PL.y
PL.y:192.25-34: warning: POSIX Yacc does not support string literals [-Wyacc]
192 | %token DISTINCT_TOK "DISTINCT"
| ^~~~~~~~~~
PL.y:193.33-37: warning: POSIX Yacc does not support string literals [-Wyacc]
193 | %token AND_TOK "AND"
| ^~~~~
PL.y:194.33-39: warning: POSIX Yacc does not support string literals [-Wyacc]
194 | %token ARRAY_TOK "ARRAY"
| ^~~~~~~
PL.y:195.33-41: warning: POSIX Yacc does not support string literals [-Wyacc]
195 | %token BOOLEAN_TOK "BOOLEAN"
| ^~~~~~~~~
PL.y:196.33-42: warning: POSIX Yacc does not support string literals [-Wyacc]
196 | %token DATATYPE_TOK "DATATYPE"
| ^~~~~~~~~~
PL.y:197.33-38: warning: POSIX Yacc does not support string literals [-Wyacc]
197 | %token ELSE_TOK "ELSE"
| ^~~~~~
PL.y:198.33-39: warning: POSIX Yacc does not support string literals [-Wyacc]
198 | %token ELSIF_TOK "ELSIF"
| ^~~~~~~
PL.y:199.33-37: warning: POSIX Yacc does not support string literals [-Wyacc]
199 | %token END_TOK "END"
| ^~~~~
PL.y:200.33-39: warning: POSIX Yacc does not support string literals [-Wyacc]
200 | %token ENDIF_TOK "ENDIF"
| ^~~~~~~
PL.y:201.33-40: warning: POSIX Yacc does not support string literals [-Wyacc]
201 | %token EXISTS_TOK "EXISTS"
| ^~~~~~~~
PL.y:202.33-39: warning: POSIX Yacc does not support string literals [-Wyacc]
202 | %token FALSELIT_TOK "FALSE"
| ^~~~~~~
PL.y:203.33-40: warning: POSIX Yacc does not support string literals [-Wyacc]
203 | %token FORALL_TOK "FORALL"
| ^~~~~~~~
PL.y:204.33-36: warning: POSIX Yacc does not support string literals [-Wyacc]
204 | %token IN_TOK "IN"
| ^~~~
PL.y:205.33-36: warning: POSIX Yacc does not support string literals [-Wyacc]
205 | %token IF_TOK "IF"
| ^~~~
PL.y:206.33-40: warning: POSIX Yacc does not support string literals [-Wyacc]
206 | %token LAMBDA_TOK "LAMBDA"
| ^~~~~~~~
PL.y:207.33-42: warning: POSIX Yacc does not support string literals [-Wyacc]
207 | %token SIMULATE_TOK "SIMULATE"
| ^~~~~~~~~~
PL.y:208.33-37: warning: POSIX Yacc does not support string literals [-Wyacc]
208 | %token LET_TOK "LET"
| ^~~~~
PL.y:209.33-37: warning: POSIX Yacc does not support string literals [-Wyacc]
209 | %token NOT_TOK "NOT"
| ^~~~~
PL.y:210.33-44: warning: POSIX Yacc does not support string literals [-Wyacc]
210 | %token IS_INTEGER_TOK "IS_INTEGER"
| ^~~~~~~~~~~~
PL.y:211.33-36: warning: POSIX Yacc does not support string literals [-Wyacc]
211 | %token OF_TOK "OF"
| ^~~~
PL.y:212.33-36: warning: POSIX Yacc does not support string literals [-Wyacc]
212 | %token OR_TOK "OR"
| ^~~~
PL.y:213.33-38: warning: POSIX Yacc does not support string literals [-Wyacc]
213 | %token REAL_TOK "REAL"
| ^~~~~~
PL.y:214.33-37: warning: POSIX Yacc does not support string literals [-Wyacc]
214 | %token INT_TOK "INT"
| ^~~~~
PL.y:215.33-41: warning: POSIX Yacc does not support string literals [-Wyacc]
215 | %token SUBTYPE_TOK "SUBTYPE"
| ^~~~~~~~~
PL.y:216.33-43: warning: POSIX Yacc does not support string literals [-Wyacc]
216 | %token BITVECTOR_TOK "BITVECTOR"
| ^~~~~~~~~~~
PL.y:217.33-38: warning: POSIX Yacc does not support string literals [-Wyacc]
217 | %token THEN_TOK "THEN"
| ^~~~~~
PL.y:218.33-38: warning: POSIX Yacc does not support string literals [-Wyacc]
218 | %token TRUELIT_TOK "TRUE"
| ^~~~~~
PL.y:219.33-38: warning: POSIX Yacc does not support string literals [-Wyacc]
219 | %token TYPE_TOK "TYPE"
| ^~~~~~
PL.y:220.33-38: warning: POSIX Yacc does not support string literals [-Wyacc]
220 | %token WITH_TOK "WITH"
| ^~~~~~
PL.y:221.33-37: warning: POSIX Yacc does not support string literals [-Wyacc]
221 | %token XOR_TOK "XOR"
| ^~~~~
PL.y:222.33-37: warning: POSIX Yacc does not support string literals [-Wyacc]
222 | %token TCC_TOK "TCC"
| ^~~~~
PL.y:223.33-41: warning: POSIX Yacc does not support string literals [-Wyacc]
223 | %token PATTERN_TOK "PATTERN"
| ^~~~~~~~~
PL.y:227.33-36: warning: POSIX Yacc does not support string literals [-Wyacc]
227 | %token DOTDOT_TOK ".."
| ^~~~
PL.y:228.33-36: warning: POSIX Yacc does not support string literals [-Wyacc]
228 | %token ASSIGN_TOK ":="
| ^~~~
PL.y:229.33-36: warning: POSIX Yacc does not support string literals [-Wyacc]
229 | %token NEQ_TOK "/="
| ^~~~
PL.y:230.33-36: warning: POSIX Yacc does not support string literals [-Wyacc]
230 | %token IMPLIES_TOK "=>"
| ^~~~
PL.y:231.33-37: warning: POSIX Yacc does not support string literals [-Wyacc]
231 | %token IFF_TOK "<=>"
| ^~~~~
PL.y:232.33-35: warning: POSIX Yacc does not support string literals [-Wyacc]
232 | %token PLUS_TOK "+"
| ^~~
PL.y:233.33-35: warning: POSIX Yacc does not support string literals [-Wyacc]
233 | %token MINUS_TOK "-"
| ^~~
PL.y:234.33-35: warning: POSIX Yacc does not support string literals [-Wyacc]
234 | %token MULT_TOK "*"
| ^~~
PL.y:235.33-35: warning: POSIX Yacc does not support string literals [-Wyacc]
235 | %token POW_TOK "^"
| ^~~
PL.y:236.33-35: warning: POSIX Yacc does not support string literals [-Wyacc]
236 | %token DIV_TOK "/"
| ^~~
PL.y:237.33-37: warning: POSIX Yacc does not support string literals [-Wyacc]
237 | %token MOD_TOK "MOD"
| ^~~~~
PL.y:238.33-37: warning: POSIX Yacc does not support string literals [-Wyacc]
238 | %token INTDIV_TOK "DIV"
| ^~~~~
PL.y:239.33-35: warning: POSIX Yacc does not support string literals [-Wyacc]
239 | %token LT_TOK "<"
| ^~~
PL.y:240.33-36: warning: POSIX Yacc does not support string literals [-Wyacc]
240 | %token LE_TOK "<="
| ^~~~
PL.y:241.33-35: warning: POSIX Yacc does not support string literals [-Wyacc]
241 | %token GT_TOK ">"
| ^~~
PL.y:242.33-36: warning: POSIX Yacc does not support string literals [-Wyacc]
242 | %token GE_TOK ">="
| ^~~~
PL.y:243.33-39: warning: POSIX Yacc does not support string literals [-Wyacc]
243 | %token FLOOR_TOK "FLOOR"
| ^~~~~~~
PL.y:244.34-37: warning: POSIX Yacc does not support string literals [-Wyacc]
244 | %token LEFTSHIFT_TOK "<<"
| ^~~~
PL.y:245.34-37: warning: POSIX Yacc does not support string literals [-Wyacc]
245 | %token RIGHTSHIFT_TOK ">>"
| ^~~~
PL.y:246.33-40: warning: POSIX Yacc does not support string literals [-Wyacc]
246 | %token BVPLUS_TOK "BVPLUS"
| ^~~~~~~~
PL.y:247.33-39: warning: POSIX Yacc does not support string literals [-Wyacc]
247 | %token BVSUB_TOK "BVSUB"
| ^~~~~~~
PL.y:248.33-40: warning: POSIX Yacc does not support string literals [-Wyacc]
248 | %token BVUDIV_TOK "BVUDIV"
| ^~~~~~~~
PL.y:249.33-40: warning: POSIX Yacc does not support string literals [-Wyacc]
249 | %token BVSDIV_TOK "BVSDIV"
| ^~~~~~~~
PL.y:250.33-40: warning: POSIX Yacc does not support string literals [-Wyacc]
250 | %token BVUREM_TOK "BVUREM"
| ^~~~~~~~
PL.y:251.33-40: warning: POSIX Yacc does not support string literals [-Wyacc]
251 | %token BVSREM_TOK "BVSREM"
| ^~~~~~~~
PL.y:252.33-40: warning: POSIX Yacc does not support string literals [-Wyacc]
252 | %token BVSMOD_TOK "BVSMOD"
| ^~~~~~~~
PL.y:253.33-39: warning: POSIX Yacc does not support string literals [-Wyacc]
253 | %token BVSHL_TOK "BVSHL"
| ^~~~~~~
PL.y:254.33-40: warning: POSIX Yacc does not support string literals [-Wyacc]
254 | %token BVASHR_TOK "BVASHR"
| ^~~~~~~~
PL.y:255.33-40: warning: POSIX Yacc does not support string literals [-Wyacc]
255 | %token BVLSHR_TOK "BVLSHR"
| ^~~~~~~~
PL.y:256.33-42: warning: POSIX Yacc does not support string literals [-Wyacc]
256 | %token BVUMINUS_TOK "BVUMINUS"
| ^~~~~~~~~~
PL.y:257.33-40: warning: POSIX Yacc does not support string literals [-Wyacc]
257 | %token BVMULT_TOK "BVMULT"
| ^~~~~~~~
PL.y:258.33-36: warning: POSIX Yacc does not support string literals [-Wyacc]
258 | %token SQHASH_TOK "[#"
| ^~~~
PL.y:259.33-36: warning: POSIX Yacc does not support string literals [-Wyacc]
259 | %token HASHSQ_TOK "#]"
| ^~~~
PL.y:260.33-36: warning: POSIX Yacc does not support string literals [-Wyacc]
260 | %token PARENHASH_TOK "(#"
| ^~~~
PL.y:261.33-36: warning: POSIX Yacc does not support string literals [-Wyacc]
261 | %token HASHPAREN_TOK "#)"
| ^~~~
PL.y:262.33-36: warning: POSIX Yacc does not support string literals [-Wyacc]
262 | %token ARROW_TOK "->"
| ^~~~
PL.y:263.33-35: warning: POSIX Yacc does not support string literals [-Wyacc]
263 | %token BVNEG_TOK "~"
| ^~~
PL.y:264.33-35: warning: POSIX Yacc does not support string literals [-Wyacc]
264 | %token BVAND_TOK "&"
| ^~~
PL.y:265.33-35: warning: POSIX Yacc does not support string literals [-Wyacc]
265 | %token MID_TOK "|"
| ^~~
PL.y:266.33-39: warning: POSIX Yacc does not support string literals [-Wyacc]
266 | %token BVXOR_TOK "BVXOR"
| ^~~~~~~
PL.y:267.33-40: warning: POSIX Yacc does not support string literals [-Wyacc]
267 | %token BVNAND_TOK "BVNAND"
| ^~~~~~~~
PL.y:268.33-39: warning: POSIX Yacc does not support string literals [-Wyacc]
268 | %token BVNOR_TOK "BVNOR"
| ^~~~~~~
PL.y:269.33-40: warning: POSIX Yacc does not support string literals [-Wyacc]
269 | %token BVCOMP_TOK "BVCOMP"
| ^~~~~~~~
PL.y:270.33-40: warning: POSIX Yacc does not support string literals [-Wyacc]
270 | %token BVXNOR_TOK "BVXNOR"
| ^~~~~~~~
PL.y:271.33-35: warning: POSIX Yacc does not support string literals [-Wyacc]
271 | %token CONCAT_TOK "@"
| ^~~
PL.y:272.33-41: warning: POSIX Yacc does not support string literals [-Wyacc]
272 | %token BVTOINT_TOK "BVTOINT"
| ^~~~~~~~~
PL.y:273.33-41: warning: POSIX Yacc does not support string literals [-Wyacc]
273 | %token INTTOBV_TOK "INTTOBV"
| ^~~~~~~~~
PL.y:274.33-45: warning: POSIX Yacc does not support string literals [-Wyacc]
274 | %token BOOLEXTRACT_TOK "BOOLEXTRACT"
| ^~~~~~~~~~~~~
PL.y:275.33-38: warning: POSIX Yacc does not support string literals [-Wyacc]
275 | %token BVLT_TOK "BVLT"
| ^~~~~~
PL.y:276.33-38: warning: POSIX Yacc does not support string literals [-Wyacc]
276 | %token BVGT_TOK "BVGT"
| ^~~~~~
PL.y:277.33-38: warning: POSIX Yacc does not support string literals [-Wyacc]
277 | %token BVLE_TOK "BVLE"
| ^~~~~~
PL.y:278.33-38: warning: POSIX Yacc does not support string literals [-Wyacc]
278 | %token BVGE_TOK "BVGE"
| ^~~~~~
PL.y:279.33-36: warning: POSIX Yacc does not support string literals [-Wyacc]
279 | %token SX_TOK "SX"
| ^~~~
PL.y:280.33-46: warning: POSIX Yacc does not support string literals [-Wyacc]
280 | %token BVZEROEXTEND_TOK "BVZEROEXTEND"
| ^~~~~~~~~~~~~~
PL.y:281.33-42: warning: POSIX Yacc does not support string literals [-Wyacc]
281 | %token BVREPEAT_TOK "BVREPEAT"
| ^~~~~~~~~~
PL.y:282.33-40: warning: POSIX Yacc does not support string literals [-Wyacc]
282 | %token BVROTL_TOK "BVROTL"
| ^~~~~~~~
PL.y:283.33-40: warning: POSIX Yacc does not support string literals [-Wyacc]
283 | %token BVROTR_TOK "BVROTR"
| ^~~~~~~~
PL.y:284.33-39: warning: POSIX Yacc does not support string literals [-Wyacc]
284 | %token BVSLT_TOK "BVSLT"
| ^~~~~~~
PL.y:285.33-39: warning: POSIX Yacc does not support string literals [-Wyacc]
285 | %token BVSGT_TOK "BVSGT"
| ^~~~~~~
PL.y:286.33-39: warning: POSIX Yacc does not support string literals [-Wyacc]
286 | %token BVSLE_TOK "BVSLE"
| ^~~~~~~
PL.y:287.33-39: warning: POSIX Yacc does not support string literals [-Wyacc]
287 | %token BVSGE_TOK "BVSGE"
| ^~~~~~~
PL.y:291.33-49: warning: POSIX Yacc does not support string literals [-Wyacc]
291 | %token ARITH_VAR_ORDER_TOK "ARITH_VAR_ORDER"
| ^~~~~~~~~~~~~~~~~
PL.y:292.33-40: warning: POSIX Yacc does not support string literals [-Wyacc]
292 | %token ASSERT_TOK "ASSERT"
| ^~~~~~~~
PL.y:293.33-39: warning: POSIX Yacc does not support string literals [-Wyacc]
293 | %token QUERY_TOK "QUERY"
| ^~~~~~~
PL.y:294.33-42: warning: POSIX Yacc does not support string literals [-Wyacc]
294 | %token CHECKSAT_TOK "CHECKSAT"
| ^~~~~~~~~~
PL.y:295.33-42: warning: POSIX Yacc does not support string literals [-Wyacc]
295 | %token CONTINUE_TOK "CONTINUE"
| ^~~~~~~~~~
PL.y:296.33-41: warning: POSIX Yacc does not support string literals [-Wyacc]
296 | %token RESTART_TOK "RESTART"
| ^~~~~~~~~
PL.y:297.33-38: warning: POSIX Yacc does not support string literals [-Wyacc]
297 | %token HELP_TOK "HELP"
| ^~~~~~
PL.y:298.33-37: warning: POSIX Yacc does not support string literals [-Wyacc]
298 | %token DBG_TOK "DBG"
| ^~~~~
PL.y:299.33-39: warning: POSIX Yacc does not support string literals [-Wyacc]
299 | %token TRACE_TOK "TRACE"
| ^~~~~~~
PL.y:300.33-41: warning: POSIX Yacc does not support string literals [-Wyacc]
300 | %token UNTRACE_TOK "UNTRACE"
| ^~~~~~~~~
PL.y:301.33-40: warning: POSIX Yacc does not support string literals [-Wyacc]
301 | %token OPTION_TOK "OPTION"
| ^~~~~~~~
PL.y:302.33-43: warning: POSIX Yacc does not support string literals [-Wyacc]
302 | %token TRANSFORM_TOK "TRANSFORM"
| ^~~~~~~~~~~
PL.y:303.33-39: warning: POSIX Yacc does not support string literals [-Wyacc]
303 | %token PRINT_TOK "PRINT"
| ^~~~~~~
PL.y:304.33-44: warning: POSIX Yacc does not support string literals [-Wyacc]
304 | %token PRINT_TYPE_TOK "PRINT_TYPE"
| ^~~~~~~~~~~~
PL.y:305.33-38: warning: POSIX Yacc does not support string literals [-Wyacc]
305 | %token CALL_TOK "CALL"
| ^~~~~~
PL.y:306.33-38: warning: POSIX Yacc does not support string literals [-Wyacc]
306 | %token ECHO_TOK "ECHO"
| ^~~~~~
PL.y:307.33-41: warning: POSIX Yacc does not support string literals [-Wyacc]
307 | %token INCLUDE_TOK "INCLUDE"
| ^~~~~~~~~
PL.y:308.33-44: warning: POSIX Yacc does not support string literals [-Wyacc]
308 | %token DUMP_PROOF_TOK "DUMP_PROOF"
| ^~~~~~~~~~~~
PL.y:309.33-50: warning: POSIX Yacc does not support string literals [-Wyacc]
309 | %token DUMP_ASSUMPTIONS_TOK "DUMP_ASSUMPTIONS"
| ^~~~~~~~~~~~~~~~~~
PL.y:310.33-42: warning: POSIX Yacc does not support string literals [-Wyacc]
310 | %token DUMP_SIG_TOK "DUMP_SIG"
| ^~~~~~~~~~
PL.y:311.33-42: warning: POSIX Yacc does not support string literals [-Wyacc]
311 | %token DUMP_TCC_TOK "DUMP_TCC"
| ^~~~~~~~~~
PL.y:312.34-55: warning: POSIX Yacc does not support string literals [-Wyacc]
312 | %token DUMP_TCC_ASSUMPTIONS_TOK "DUMP_TCC_ASSUMPTIONS"
| ^~~~~~~~~~~~~~~~~~~~~~
PL.y:313.33-48: warning: POSIX Yacc does not support string literals [-Wyacc]
313 | %token DUMP_TCC_PROOF_TOK "DUMP_TCC_PROOF"
| ^~~~~~~~~~~~~~~~
PL.y:314.33-46: warning: POSIX Yacc does not support string literals [-Wyacc]
314 | %token DUMP_CLOSURE_TOK "DUMP_CLOSURE"
| ^~~~~~~~~~~~~~
PL.y:315.33-52: warning: POSIX Yacc does not support string literals [-Wyacc]
315 | %token DUMP_CLOSURE_PROOF_TOK "DUMP_CLOSURE_PROOF"
| ^~~~~~~~~~~~~~~~~~~~
PL.y:316.33-39: warning: POSIX Yacc does not support string literals [-Wyacc]
316 | %token WHERE_TOK "WHERE"
| ^~~~~~~
PL.y:317.33-44: warning: POSIX Yacc does not support string literals [-Wyacc]
317 | %token ASSERTIONS_TOK "ASSERTIONS"
| ^~~~~~~~~~~~
PL.y:318.33-45: warning: POSIX Yacc does not support string literals [-Wyacc]
318 | %token ASSUMPTIONS_TOK "ASSUMPTIONS"
| ^~~~~~~~~~~~~
PL.y:319.33-48: warning: POSIX Yacc does not support string literals [-Wyacc]
319 | %token COUNTEREXAMPLE_TOK "COUNTEREXAMPLE"
| ^~~~~~~~~~~~~~~~
PL.y:320.33-46: warning: POSIX Yacc does not support string literals [-Wyacc]
320 | %token COUNTERMODEL_TOK "COUNTERMODEL"
| ^~~~~~~~~~~~~~
PL.y:321.33-38: warning: POSIX Yacc does not support string literals [-Wyacc]
321 | %token PUSH_TOK "PUSH"
| ^~~~~~
PL.y:322.33-37: warning: POSIX Yacc does not support string literals [-Wyacc]
322 | %token POP_TOK "POP"
| ^~~~~
PL.y:323.33-39: warning: POSIX Yacc does not support string literals [-Wyacc]
323 | %token POPTO_TOK "POPTO"
| ^~~~~~~
PL.y:324.33-44: warning: POSIX Yacc does not support string literals [-Wyacc]
324 | %token PUSH_SCOPE_TOK "PUSH_SCOPE"
| ^~~~~~~~~~~~
PL.y:325.33-43: warning: POSIX Yacc does not support string literals [-Wyacc]
325 | %token POP_SCOPE_TOK "POP_SCOPE"
| ^~~~~~~~~~~
PL.y:326.33-45: warning: POSIX Yacc does not support string literals [-Wyacc]
326 | %token POPTO_SCOPE_TOK "POPTO_SCOPE"
| ^~~~~~~~~~~~~
PL.y:327.33-39: warning: POSIX Yacc does not support string literals [-Wyacc]
327 | %token RESET_TOK "RESET"
| ^~~~~~~
PL.y:328.33-41: warning: POSIX Yacc does not support string literals [-Wyacc]
328 | %token CONTEXT_TOK "CONTEXT"
| ^~~~~~~~~
PL.y:329.33-40: warning: POSIX Yacc does not support string literals [-Wyacc]
329 | %token FORGET_TOK "FORGET"
| ^~~~~~~~
PL.y:330.33-42: warning: POSIX Yacc does not support string literals [-Wyacc]
330 | %token GET_TYPE_TOK "GET_TYPE"
| ^~~~~~~~~~
PL.y:331.33-44: warning: POSIX Yacc does not support string literals [-Wyacc]
331 | %token CHECK_TYPE_TOK "CHECK_TYPE"
| ^~~~~~~~~~~~
PL.y:332.33-43: warning: POSIX Yacc does not support string literals [-Wyacc]
332 | %token GET_CHILD_TOK "GET_CHILD"
| ^~~~~~~~~~~
PL.y:333.33-40: warning: POSIX Yacc does not support string literals [-Wyacc]
333 | %token GET_OP_TOK "GET_OP"
| ^~~~~~~~
PL.y:334.33-44: warning: POSIX Yacc does not support string literals [-Wyacc]
334 | %token SUBSTITUTE_TOK "SUBSTITUTE"
| ^~~~~~~~~~~~
PL.y: warning: 3 shift/reduce conflicts [-Wconflicts-sr]
PL.y: note: rerun with option '-Wcounterexamples' to generate conflict counterexamples
PL.y:1531.24-1536.25: warning: rule useless in parser due to conflicts [-Wother]
1531 | AndExpr : AndExpr AND_TOK Expr
| ^~~~~~~~~~~~~~~~~~~~
PL.y:1549.25-1554.25: warning: rule useless in parser due to conflicts [-Wother]
1549 | OrExpr : OrExpr OR_TOK Expr
| ^~~~~~~~~~~~~~~~~~
flex -I -PPL -olexPL.cpp PL.lex
bison -d -y -o parseLisp.cpp -p Lisp --debug -v Lisp.y
Lisp.y:75.33-36: warning: POSIX Yacc does not support string literals [-Wyacc]
75 | %token BINARY_TOK "0b"
| ^~~~
Lisp.y:76.33-36: warning: POSIX Yacc does not support string literals [-Wyacc]
76 | %token HEX_TOK "0x"
| ^~~~
flex -I -PLisp -olexLisp.cpp Lisp.lex
bison -d -y -o parsesmtlib.cpp -p smtlib --debug -v smtlib.y
flex -I -Psmtlib -olexsmtlib.cpp smtlib.lex
bison -d -y -o parsesmtlib2.cpp -p smtlib2 --debug -v smtlib2.y
smtlib2.y: warning: 4 shift/reduce conflicts [-Wconflicts-sr]
smtlib2.y: note: rerun with option '-Wcounterexamples' to generate conflict counterexamples
flex -I -Psmtlib2 -olexsmtlib2.cpp smtlib2.lex
Making dependencies for parsePL.cpp lexPL.cpp parseLisp.cpp lexLisp.cpp parsesmtlib.cpp lexsmtlib.cpp parsesmtlib2.cpp lexsmtlib2.cpp parser.cpp
g++ -M -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -O0 parsePL.cpp lexPL.cpp parseLisp.cpp lexLisp.cpp parsesmtlib.cpp lexsmtlib.cpp parsesmtlib2.cpp lexsmtlib2.cpp parser.cpp >> /build/cvc3-2.4.1/obj/parser/x86_64-linux-gnu/Makefile.tmp
parsePL.cpp:278:10: fatal error: parsePL.hpp: No such file or directory
278 | #include "parsePL.hpp"
| ^~~~~~~~~~~~~
compilation terminated.
parseLisp.cpp:161:10: fatal error: parseLisp.hpp: No such file or directory
161 | #include "parseLisp.hpp"
| ^~~~~~~~~~~~~~~
compilation terminated.
parsesmtlib.cpp:170:10: fatal error: parsesmtlib.hpp: No such file or directory
170 | #include "parsesmtlib.hpp"
| ^~~~~~~~~~~~~~~~~
compilation terminated.
parsesmtlib2.cpp:170:10: fatal error: parsesmtlib2.hpp: No such file or directory
170 | #include "parsesmtlib2.hpp"
| ^~~~~~~~~~~~~~~~~~
compilation terminated.
make[3]: *** [/build/cvc3-2.4.1/Makefile.std:279: depend] Error 1
g++ -m64 -fPIC -O2 -Wall -I. -I/build/cvc3-2.4.1/src/include -O0 -c parsePL.cpp -o '/build/cvc3-2.4.1/obj/parser/x86_64-linux-gnu/parsePL.o'
In file included from /nix/store/bgvxpx97q789xc8rrginprlvk8p03p93-glibc-2.31-dev/include/bits/libc-header-start.h:33,
from /nix/store/bgvxpx97q789xc8rrginprlvk8p03p93-glibc-2.31-dev/include/stdint.h:26,
from /nix/store/rclksjxdjgp6y6qkxyl9m4dx4b9d45zk-gcc-9.3.0/lib/gcc/x86_64-unknown-linux-gnu/9.3.0/include/stdint.h:9,
from /build/cvc3-2.4.1/src/include/os.h:75,
from /build/cvc3-2.4.1/src/include/vc.h:25,
from PL.y:28:
/nix/store/bgvxpx97q789xc8rrginprlvk8p03p93-glibc-2.31-dev/include/features.h:397:4: warning: #warning _FORTIFY_SOURCE requires compiling with optimization (-O) [-Wcpp]
397 | # warning _FORTIFY_SOURCE requires compiling with optimization (-O)
| ^~~~~~~
parsePL.cpp:278:10: fatal error: parsePL.hpp: No such file or directory
278 | #include "parsePL.hpp"
| ^~~~~~~~~~~~~
compilation terminated.
make[2]: *** [/build/cvc3-2.4.1/Makefile.std:194: /build/cvc3-2.4.1/obj/parser/x86_64-linux-gnu/parsePL.o] Error 1
make[2]: Leaving directory '/build/cvc3-2.4.1/src/parser'
make[1]: *** [Makefile:171: build] Error 2
make[1]: Leaving directory '/build/cvc3-2.4.1/src'
make: *** [Makefile:44: build] Error 2
builder for '/nix/store/caakrmqy90qfh8gaf4k5n90m95v12gq7-cvc3-2.4.1.drv' failed with exit code 2
error: build of '/nix/store/4nvdir1hgksyp8az26yizsh22b0x3xbg-vscode-with-extensions-1.48.2.drv', '/nix/store/66ljz3vnvyx2vnl5jpgpss10h67m7f0p-archetype-development.drv', '/nix/store/bhdxnh1bx2cix4gakd4lzqc56wqqpmqw-why3-1.3.2.drv', '/nix/store/caakrmqy90qfh8gaf4k5n90m95v12gq7-cvc3-2.4.1.drv', '/nix/store/lgm44196b0rafawlg0haa2dcn7gbn07n-ocaml4.10.0-alt-ergo-2.3.3.drv' failed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment