Blob Blame History Raw
Index: src/cbmc/Makefile
===================================================================
--- src/cbmc/Makefile	(revision 5391)
+++ src/cbmc/Makefile	(working copy)
@@ -23,7 +23,7 @@
 
 INCLUDES= -I ..
 
-LIBS =
+LIBS = -lminisat -lcuddobj -lcudd -lmtr -lcuddst -lcuddutil -lepd -ldddmp
 
 include ../config.inc
 include ../common
Index: src/common
===================================================================
--- src/common	(revision 5391)
+++ src/common	(working copy)
@@ -69,7 +69,7 @@
   endif
 else
   LINKLIB = ar rcT $@ $^
-  LINKBIN = $(CXX) $(LINKFLAGS) -o $@ -Wl,--start-group $^ -Wl,--end-group $(LIBS)
+  LINKBIN = $(CXX) $(LINKFLAGS) -o $@ -Wl,--start-group $^ -Wl,--end-group $(LDFLAGS) $(LIBS)
   LINKNATIVE = $(HOSTCXX) -o $@ $^
   ifeq ($(origin CC),default)
     CC     = gcc
Index: src/config.inc
===================================================================
--- src/config.inc	(revision 5391)
+++ src/config.inc	(working copy)
@@ -4,18 +4,22 @@
 # Variables you may want to override
 #CXXFLAGS = -Wall -O0 -g -Werror -Wno-long-long -Wno-sign-compare -Wno-parentheses -Wno-strict-aliasing -pedantic
 #CXXFLAGS = -std=c++11
+CFLAGS = @RPM_OPT_FLAGS@
+CXXFLAGS = @RPM_OPT_FLAGS@
+LDFLAGS = @RPM_LD_FLAGS@
 
 # If GLPK is available; this is used by goto-instrument and musketeer.
-#LIB_GLPK = -lglpk 
+LIB_GLPK = -lglpk 
 
 # SAT-solvers we have
 #PRECOSAT = ../../precosat-576-7e5e66f-120112
 #PICOSAT = ../../picosat-959
+CUDD = /usr
 #LINGELING = ../../lingeling-587f-4882048-110513
 #CHAFF = ../../zChaff
 #BOOLEFORCE = ../../booleforce-0.4
 #MINISAT = ../../MiniSat-p_v1.14
-MINISAT2 = ../../minisat-2.2.0
+MINISAT2 = /usr/include/minisat
 #GLUCOSE = ../../glucose2.2
 #SMVSAT =
 
Index: src/goto-instrument/Makefile
===================================================================
--- src/goto-instrument/Makefile	(revision 5391)
+++ src/goto-instrument/Makefile	(working copy)
@@ -39,7 +39,7 @@
 
 INCLUDES= -I ..
 
-LIBS = 
+LIBS = -lminisat -lcuddobj -lcudd -lmtr -lcuddst -lcuddutil -lepd -ldddmp
 
 CLEANFILES = goto-instrument$(EXEEXT)
 
Index: src/solvers/Makefile
===================================================================
--- src/solvers/Makefile	(revision 5391)
+++ src/solvers/Makefile	(working copy)
@@ -17,7 +17,7 @@
 ifneq ($(MINISAT2),)
   MINISAT2_SRC=sat/satcheck_minisat2.cpp
   MINISAT2_INCLUDE=-I $(MINISAT2)
-  MINISAT2_LIB=$(MINISAT2)/simp/SimpSolver$(OBJEXT) $(MINISAT2)/core/Solver$(OBJEXT)
+#  MINISAT2_LIB=$(MINISAT2)/simp/SimpSolver$(OBJEXT) $(MINISAT2)/core/Solver$(OBJEXT)
   CP_CXXFLAGS += -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS
   override CXXFLAGS := $(filter-out -pedantic, $(CXXFLAGS))
 endif
@@ -44,10 +44,10 @@
 
 ifneq ($(CUDD),)
   CUDD_SRC=qbf/qbf_bdd_core.cpp qbf/qbf_skizzo_core.cpp
-  CUDD_INCLUDE=-I $(CUDD)/include
-  CUDD_LIB=-L $(CUDD)/cudd -L $(CUDD)/util -L $(CUDD)/mtr \
-           -L $(CUDD)/st -L $(CUDD)/obj -L $(CUDD)/dddmp \
-           -L $(CUDD)/epd -lobj -lcudd -lmtr -lst -lutil -lepd -ldddmp
+  CUDD_INCLUDE=-I $(CUDD)/include/cudd
+#  CUDD_LIB=-L $(CUDD)/cudd -L $(CUDD)/util -L $(CUDD)/mtr \
+#           -L $(CUDD)/st -L $(CUDD)/obj -L $(CUDD)/dddmp \
+#           -L $(CUDD)/epd -lobj -lcudd -lmtr -lst -lutil -lepd -ldddmp
 endif
 
 ifneq ($(PRECOSAT),)