diff --git a/jbmc/src/janalyzer/Makefile b/jbmc/src/janalyzer/Makefile index 879939a34d..f1fc8fcf0f 100644 --- a/jbmc/src/janalyzer/Makefile +++ b/jbmc/src/janalyzer/Makefile @@ -11,6 +11,7 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \ ../$(CPROVER_DIR)/src/pointer-analysis/pointer-analysis$(LIBEXT) \ ../$(CPROVER_DIR)/src/langapi/langapi$(LIBEXT) \ ../$(CPROVER_DIR)/src/json/json$(LIBEXT) \ + ../$(CPROVER_DIR)/src/solvers/solvers$(LIBEXT) \ ../$(CPROVER_DIR)/src/util/util$(LIBEXT) \ ..//miniz/miniz$(OBJEXT) \ ../$(CPROVER_DIR)/src/goto-analyzer/static_show_domain$(OBJEXT) \ diff --git a/jbmc/src/jdiff/Makefile b/jbmc/src/jdiff/Makefile index 2bb2c551e1..4ceab46259 100644 --- a/jbmc/src/jdiff/Makefile +++ b/jbmc/src/jdiff/Makefile @@ -28,6 +28,7 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \ ../$(CPROVER_DIR)/src/analyses/analyses$(LIBEXT) \ ../$(CPROVER_DIR)/src/langapi/langapi$(LIBEXT) \ ../$(CPROVER_DIR)/src/xmllang/xmllang$(LIBEXT) \ + ../$(CPROVER_DIR)/src/solvers/solvers$(LIBEXT) \ ../$(CPROVER_DIR)/src/util/util$(LIBEXT) \ ../miniz/miniz$(OBJEXT) \ ../$(CPROVER_DIR)/src/json/json$(LIBEXT) \ diff --git a/src/analyses/Makefile b/src/analyses/Makefile index 3e52255c82..07f8daf231 100644 --- a/src/analyses/Makefile +++ b/src/analyses/Makefile @@ -41,6 +41,10 @@ CLEANFILES = analyses$(LIBEXT) all: analyses$(LIBEXT) +ifneq ($(CUDD),) + OBJ += $(CUDD)/cudd/.libs/libcudd$(LIBEXT) $(CUDD)/cplusplus/.libs/libobj$(LIBEXT) +endif + ############################################################################### analyses$(LIBEXT): $(OBJ) diff --git a/src/common b/src/common index 080a157b69..075952f2d0 100644 --- a/src/common +++ b/src/common @@ -195,6 +195,16 @@ ifneq ($(CADICAL),) endif +ifneq ($(CUDD),) + CP_CXXFLAGS += -DHAVE_CUDD +ifeq ($(CPROVER_DIR),) + INCLUDES += -I $(CUDD) -I $(CUDD)/cudd +else + INCLUDES += -I ../$(CPROVER_DIR)/src/solvers/$(CUDD) + INCLUDES += -I ../$(CPROVER_DIR)/src/solvers/$(CUDD)/cudd +endif +endif + first_target: all diff --git a/src/goto-analyzer/Makefile b/src/goto-analyzer/Makefile index 6e69ea1ce9..ad955380c4 100644 --- a/src/goto-analyzer/Makefile +++ b/src/goto-analyzer/Makefile @@ -19,6 +19,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../langapi/langapi$(LIBEXT) \ ../json/json$(LIBEXT) \ ../assembler/assembler$(LIBEXT) \ + ../solvers/solvers$(LIBEXT) \ ../util/util$(LIBEXT) \ # Empty last line diff --git a/src/solvers/Makefile b/src/solvers/Makefile index fd5e9bedb3..56c4362006 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -44,9 +44,7 @@ ifneq ($(SQUOLEM2),) endif ifneq ($(CUDD),) - CUDD_INCLUDE=-I $(CUDD) CUDD_LIB=$(CUDD)/cudd/.libs/libcudd$(LIBEXT) $(CUDD)/cplusplus/.libs/libobj$(LIBEXT) - CP_CXXFLAGS += -DHAVE_CUDD endif ifneq ($(PICOSAT),) diff --git a/unit/Makefile b/unit/Makefile index 8b3f5343b1..824ebd1c99 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -84,6 +84,7 @@ SRC += analyses/ai/ai.cpp \ INCLUDES= -I ../src/ -I. +CPROVER_DIR = . include ../src/config.inc include ../src/common