Skip to content

Instantly share code, notes, and snippets.

@LeventErkok
Created December 17, 2016 18:33
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save LeventErkok/a1fb199b83131f6db8e2a51c9b285816 to your computer and use it in GitHub Desktop.
Save LeventErkok/a1fb199b83131f6db8e2a51c9b285816 to your computer and use it in GitHub Desktop.
rm -rf lingeling*
tar xf archives/lingeling*.tar.gz
mv lingeling* lingeling
cd lingeling && ./configure.sh && make
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA -c lglib.c
lglib.c:19486:7: warning: variable 'res' is used uninitialized whenever 'if' condition is false
[-Wsometimes-uninitialized]
if (lglgaussextractexactly1 (lgl, c)) res = 1;
^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
lglib.c:19492:10: note: uninitialized use occurs here
return res;
^~~
lglib.c:19486:3: note: remove the 'if' if its condition is always true
if (lglgaussextractexactly1 (lgl, c)) res = 1;
^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~
lglib.c:19485:10: note: initialize the variable 'res' to silence this warning
int res;
^
= 0
1 warning generated.
Configured with: --prefix=/Applications/Xcode.app/Contents/Developer/usr --with-gxx-include-dir=/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX10.11.sdk/usr/include/c++/4.2.1
rm -f lglcflags.h
echo '#define LGL_CC "Apple LLVM version 7.0.0 (clang-700.1.76)"' >> lglcflags.h
echo '#define LGL_CFLAGS "-Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA"' >> lglcflags.h
rm -f lglcfg.h
./mkconfig.sh > lglcfg.h
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA -c lglbnr.c
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA -c lgldimacs.c
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA -c lglopts.c
ar rc liblgl.a lglib.o lglbnr.o lgldimacs.o lglopts.o
ranlib liblgl.a
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA -c lglmain.c
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA -o lingeling lglmain.o -L. -llgl -lm
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA -c plingeling.c
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA -pthread -o plingeling plingeling.o -L. -llgl -lm
clang: warning: argument unused during compilation: '-pthread'
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA -c ilingeling.c
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA -pthread -o ilingeling ilingeling.o -L. -llgl -lm
clang: warning: argument unused during compilation: '-pthread'
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA -c treengeling.c
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA -pthread -o treengeling treengeling.o -L. -llgl -lm
clang: warning: argument unused during compilation: '-pthread'
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA -c lglmbt.c
lglmbt.c:729:20: warning: taking the absolute value of unsigned type 'unsigned int' has no effect
[-Wabsolute-value]
prev = env.seed = abs (env.seed) >> 1;
^
lglmbt.c:729:20: note: remove the call to 'abs' since unsigned values cannot be negative
prev = env.seed = abs (env.seed) >> 1;
^~~~
1 warning generated.
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA -o lglmbt lglmbt.o -L. -llgl -lm
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA -c lgluntrace.c
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA -o lgluntrace lgluntrace.o -L. -llgl -lm
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA -c lglddtrace.c
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA -o lglddtrace lglddtrace.o -L. -llgl -lm
rm -rf boolector*
tar xf archives/boolector*.tar.gz
mv boolector* boolector
cd boolector && ./configure.sh && make
readlink: illegal option -- f
usage: readlink [-n] [file ...]
[configure.sh] optimized compilation (no '-g')
[configure.sh] compiling without logging support (default for no debugging)
[configure.sh] disabling PicoSAT: './../picosat' missing
[configure.sh] using Lingeling in './../lingeling'
[configure.sh] not using YalSAT
[configure.sh] not using Druplig
[configure.sh] disabling MiniSAT: './../minisat' missing
[configure.sh] linking against 'libm'
[configure.sh] CC=gcc
[configure.sh] CFLAGS=-W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING
[configure.sh] LIBS=-Wl\,-rpath\,./build -Lbuild -L./../lingeling -llgl -lm
[configure.sh] OBJS=
[configure.sh] INCS=-Isrc -Ibuild -I./../lingeling
[configure.sh] makefile generated
rm -f build/btorconfig.h
./mkconfig.sh > build/btorconfig.h
Configured with: --prefix=/Applications/Xcode.app/Contents/Developer/usr --with-gxx-include-dir=/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX10.11.sdk/usr/include/c++/4.2.1
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/btorabort.c -o build/btorabort.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/btoraig.c -o build/btoraig.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/btoraigvec.c -o build/btoraigvec.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/btorass.c -o build/btorass.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/btorbeta.c -o build/btorbeta.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/btorbitvec.c -o build/btorbitvec.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/btorchkclone.c -o build/btorchkclone.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/btorclone.c -o build/btorclone.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/btorcore.c -o build/btorcore.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/btordbg.c -o build/btordbg.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/btordcr.c -o build/btordcr.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/btorexp.c -o build/btorexp.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/btormc.c -o build/btormc.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/btormodel.c -o build/btormodel.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/btormsg.c -o build/btormsg.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/btoropt.c -o build/btoropt.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/btorparse.c -o build/btorparse.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/btorprintmodel.c -o build/btorprintmodel.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/btorrewrite.c -o build/btorrewrite.o
src/btorrewrite.c:1888:1: warning: unused function 'applies_and_and_1_eq' [-Wunused-function]
applies_and_and_1_eq (Btor * btor, BtorNode * e0, BtorNode * e1)
^
src/btorrewrite.c:1903:1: warning: unused function 'apply_and_and_1_eq' [-Wunused-function]
apply_and_and_1_eq (Btor * btor, BtorNode * e0, BtorNode * e1)
^
src/btorrewrite.c:1924:1: warning: unused function 'applies_and_and_2_eq' [-Wunused-function]
applies_and_and_2_eq (Btor * btor, BtorNode * e0, BtorNode * e1)
^
src/btorrewrite.c:1939:1: warning: unused function 'apply_and_and_2_eq' [-Wunused-function]
apply_and_and_2_eq (Btor * btor, BtorNode * e0, BtorNode * e1)
^
src/btorrewrite.c:1961:1: warning: unused function 'applies_and_and_3_eq' [-Wunused-function]
applies_and_and_3_eq (Btor * btor, BtorNode * e0, BtorNode * e1)
^
src/btorrewrite.c:1974:1: warning: unused function 'apply_and_and_3_eq' [-Wunused-function]
apply_and_and_3_eq (Btor * btor, BtorNode * e0, BtorNode * e1)
^
src/btorrewrite.c:1996:1: warning: unused function 'applies_and_and_4_eq' [-Wunused-function]
applies_and_and_4_eq (Btor * btor, BtorNode * e0, BtorNode * e1)
^
src/btorrewrite.c:2009:1: warning: unused function 'apply_and_and_4_eq' [-Wunused-function]
apply_and_and_4_eq (Btor * btor, BtorNode * e0, BtorNode * e1)
^
src/btorrewrite.c:2347:1: warning: unused function 'applies_zero_eq_and_eq' [-Wunused-function]
applies_zero_eq_and_eq (Btor * btor, BtorNode * e0, BtorNode * e1)
^
src/btorrewrite.c:2360:1: warning: unused function 'apply_zero_eq_and_eq' [-Wunused-function]
apply_zero_eq_and_eq (Btor * btor, BtorNode * e0, BtorNode * e1)
^
src/btorrewrite.c:3769:1: warning: unused function 'applies_bcond_mul' [-Wunused-function]
applies_bcond_mul (Btor * btor, BtorNode * e0, BtorNode * e1)
^
src/btorrewrite.c:3784:1: warning: unused function 'apply_bcond_mul' [-Wunused-function]
apply_bcond_mul (Btor * btor, BtorNode * e0, BtorNode * e1)
^
12 warnings generated.
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/btorsat.c -o build/btorsat.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/btorslvaigprop.c -o build/btorslvaigprop.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/btorslvfun.c -o build/btorslvfun.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/btorslvprop.c -o build/btorslvprop.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/btorslvpropsls.c -o build/btorslvpropsls.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/btorslvsls.c -o build/btorslvsls.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/btorsort.c -o build/btorsort.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/btortrapi.c -o build/btortrapi.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/dumper/btordumpaig.c -o build/dumper/btordumpaig.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/dumper/btordumpbtor.c -o build/dumper/btordumpbtor.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/dumper/btordumpsmt.c -o build/dumper/btordumpsmt.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/parser/btorbtor.c -o build/parser/btorbtor.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/parser/btorsmt.c -o build/parser/btorsmt.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/parser/btorsmt2.c -o build/parser/btorsmt2.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/simplifier/btorack.c -o build/simplifier/btorack.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/simplifier/btorelimapplies.c -o build/simplifier/btorelimapplies.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/simplifier/btorelimslices.c -o build/simplifier/btorelimslices.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/simplifier/btorextract.c -o build/simplifier/btorextract.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/simplifier/btormerge.c -o build/simplifier/btormerge.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/simplifier/btorskel.c -o build/simplifier/btorskel.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/simplifier/btorunconstrained.c -o build/simplifier/btorunconstrained.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/utils/btoraigmap.c -o build/utils/btoraigmap.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/utils/btorexpiter.c -o build/utils/btorexpiter.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/utils/btorhashint.c -o build/utils/btorhashint.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/utils/btorhashptr.c -o build/utils/btorhashptr.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/utils/btormem.c -o build/utils/btormem.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/utils/btormisc.c -o build/utils/btormisc.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/utils/btornodemap.c -o build/utils/btornodemap.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/utils/btorrng.c -o build/utils/btorrng.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/utils/btorutil.c -o build/utils/btorutil.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/boolector.c -o build/boolector.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/utils/boolectormap.c -o build/utils/boolectormap.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/aigprop.c -o build/aigprop.o
rm -f build/libboolector.a
ar rc build/libboolector.a build/btorabort.o build/btoraig.o build/btoraigvec.o build/btorass.o build/btorbeta.o build/btorbitvec.o build/btorchkclone.o build/btorclone.o build/btorcore.o build/btordbg.o build/btordcr.o build/btorexp.o build/btormc.o build/btormodel.o build/btormsg.o build/btoropt.o build/btorparse.o build/btorprintmodel.o build/btorrewrite.o build/btorsat.o build/btorslvaigprop.o build/btorslvfun.o build/btorslvprop.o build/btorslvpropsls.o build/btorslvsls.o build/btorsort.o build/btortrapi.o build/dumper/btordumpaig.o build/dumper/btordumpbtor.o build/dumper/btordumpsmt.o build/parser/btorbtor.o build/parser/btorsmt.o build/parser/btorsmt2.o build/simplifier/btorack.o build/simplifier/btorelimapplies.o build/simplifier/btorelimslices.o build/simplifier/btorextract.o build/simplifier/btormerge.o build/simplifier/btorskel.o build/simplifier/btorunconstrained.o build/utils/btoraigmap.o build/utils/btorexpiter.o build/utils/btorhashint.o build/utils/btorhashptr.o build/utils/btormem.o build/utils/btormisc.o build/utils/btornodemap.o build/utils/btorrng.o build/utils/btorutil.o build/boolector.o build/utils/boolectormap.o build/aigprop.o
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/ranlib: file: build/libboolector.a(btorchkclone.o) has no symbols
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/ranlib: file: build/libboolector.a(btordbg.o) has no symbols
ranlib build/libboolector.a
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/ranlib: file: build/libboolector.a(btorchkclone.o) has no symbols
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/ranlib: file: build/libboolector.a(btordbg.o) has no symbols
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/btormain.c -o build/btormain.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/boolectormain.c -o build/boolectormain.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -o bin/boolector build/btormain.o build/boolectormain.o build/libboolector.a ./../lingeling/liblgl.a -Wl,-rpath,./build -Lbuild -L./../lingeling -llgl -lm -lboolector
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/btorimc.cc -o build/btorimc.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/btoribv.cc -o build/btoribv.o
g++ -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -o bin/btorimc build/btorimc.o build/btoribv.o -Lbuild -lboolector -Wl,-rpath,./build -Lbuild -L./../lingeling -llgl -lm
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/btoruntrace.c -o build/btoruntrace.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -o bin/btoruntrace build/btoruntrace.o -Lbuild -lboolector -Wl,-rpath,./build -Lbuild -L./../lingeling -llgl -lm
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -c src/btormbt.c -o build/btormbt.o
gcc -W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild -I./../lingeling -o bin/btormbt build/btormbt.o -Lbuild -lboolector -Wl,-rpath,./build -Lbuild -L./../lingeling -llgl -lm
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment