Created
December 17, 2016 18:33
-
-
Save LeventErkok/a1fb199b83131f6db8e2a51c9b285816 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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