Support for separation logic. Enable cbqi by default for pure BV.

1 files changed, 9 insertions, 3 deletions

diff --git a/src/options/Makefile.am b/src/options/Makefile.am
index e8a18481b..1eb84b45f 100644
--- a/src/options/Makefile.am
+++ b/src/options/Makefile.am
@@ -30,6 +30,7 @@ OPTIONS_SRC_FILES = \
 	proof_options \
 	prop_options \
 	quantifiers_options \
+	sep_options \
 	sets_options \
 	smt_options \
 	strings_options \
@@ -54,6 +55,7 @@ OPTIONS_TEMPS = \
 	proof_options.tmp \
 	prop_options.tmp \
 	quantifiers_options.tmp \
+	sep_options.tmp \
 	sets_options.tmp \
 	smt_options.tmp \
 	strings_options.tmp \
@@ -78,6 +80,7 @@ OPTIONS_OPTIONS_FILES = \
 	proof_options.options \
 	prop_options.options \
 	quantifiers_options.options \
+	sep_options.options \
 	sets_options.options \
 	smt_options.options \
 	strings_options.options \
@@ -102,6 +105,7 @@ OPTIONS_SEDS = \
 	proof_options.sed \
 	prop_options.sed \
 	quantifiers_options.sed \
+	sep_options.sed \
 	sets_options.sed \
 	smt_options.sed \
 	strings_options.sed \
@@ -126,6 +130,7 @@ OPTIONS_HEADS = \
 	proof_options.h \
 	prop_options.h \
 	quantifiers_options.h \
+	sep_options.h \
 	sets_options.h \
 	smt_options.h \
 	strings_options.h \
@@ -150,6 +155,7 @@ OPTIONS_CPPS = \
 	proof_options.cpp \
 	prop_options.cpp \
 	quantifiers_options.cpp \
+	sep_options.cpp \
 	sets_options.cpp \
 	smt_options.cpp \
 	strings_options.cpp \
@@ -295,14 +301,14 @@ options_holder_template.h options_template.cpp options_get_option_template.cpp o
 
 # Make sure the implicit rules never mistake X_options for the -o file for a
 # CPP file.
-arith_options arrays_options base_options booleans_options builtin_options bv_options datatypes_options decision_options expr_options fp_options idl_options main_options parser_options printer_options proof_options prop_options quantifiers_options sets_options smt_options strings_options theory_options uf_options:;
+arith_options arrays_options base_options booleans_options builtin_options bv_options datatypes_options decision_options expr_options fp_options idl_options main_options parser_options printer_options proof_options prop_options quantifiers_options sep_options sets_options smt_options strings_options theory_options uf_options:;
 
 
 # These are phony to force them to be made everytime.
-.PHONY: arith_options.tmp arrays_options.tmp base_options.tmp booleans_options.tmp builtin_options.tmp bv_options.tmp datatypes_options.tmp decision_options.tmp expr_options.tmp fp_options.tmp idl_options.tmp main_options.tmp parser_options.tmp printer_options.tmp proof_options.tmp prop_options.tmp quantifiers_options.tmp sets_options.tmp smt_options.tmp strings_options.tmp theory_options.tmp uf_options.tmp
+.PHONY: arith_options.tmp arrays_options.tmp base_options.tmp booleans_options.tmp builtin_options.tmp bv_options.tmp datatypes_options.tmp decision_options.tmp expr_options.tmp fp_options.tmp idl_options.tmp main_options.tmp parser_options.tmp printer_options.tmp proof_options.tmp prop_options.tmp quantifiers_options.tmp sep_options.tmp sets_options.tmp smt_options.tmp strings_options.tmp theory_options.tmp uf_options.tmp
 
 # Make is happier being listed explictly. Not sure why.
-arith_options.tmp arrays_options.tmp base_options.tmp booleans_options.tmp builtin_options.tmp bv_options.tmp datatypes_options.tmp decision_options.tmp expr_options.tmp fp_options.tmp idl_options.tmp main_options.tmp parser_options.tmp printer_options.tmp proof_options.tmp prop_options.tmp quantifiers_options.tmp sets_options.tmp smt_options.tmp strings_options.tmp theory_options.tmp uf_options.tmp:
+arith_options.tmp arrays_options.tmp base_options.tmp booleans_options.tmp builtin_options.tmp bv_options.tmp datatypes_options.tmp decision_options.tmp expr_options.tmp fp_options.tmp idl_options.tmp main_options.tmp parser_options.tmp printer_options.tmp proof_options.tmp prop_options.tmp quantifiers_options.tmp sep_options.tmp sets_options.tmp smt_options.tmp strings_options.tmp theory_options.tmp uf_options.tmp:
 	echo "$@" "$(@:.tmp=)"
 	$(AM_V_GEN)(cp "@srcdir@/$(@:.tmp=)" "$@" || true)
 #TIM: