Merging CAV14 paper bit-vector work.

1 files changed, 11 insertions, 1 deletions

diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h
index 058a00f32..af8e8663c 100644
--- a/src/smt/options_handlers.h
+++ b/src/smt/options_handlers.h
@@ -121,7 +121,13 @@ t-explanations [non-stateful]\n\
 bv-rewrites [non-stateful]\n\
 + Output correctness queries for all bitvector rewrites\n\
 \n\
-theory::fullcheck [non-stateful]\n\
+bv-abstraction [non-stateful]\n\
++ Output correctness queries for all bv abstraction \n\
+\n\
+bv-algebraic [non-stateful]\n\
++ Output correctness queries for bv algebraic solver. \n\
+\n\
+theory::fullcheck [non-stateful]\n                                      \
 + Output completeness queries for all full-check effort-level theory checks\n\
 \n\
 Dump modes can be combined with multiple uses of --dump.  Generally you want\n\
@@ -237,6 +243,10 @@ inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) {
     } else if(!strcmp(optargPtr, "help")) {
       puts(dumpHelp.c_str());
       exit(1);
+    } else if(!strcmp(optargPtr, "bv-abstraction")) {
+      Dump.on("bv-abstraction");
+    } else if(!strcmp(optargPtr, "bv-algebraic")) {
+      Dump.on("bv-algebraic");
     } else {
       throw OptionException(std::string("unknown option for --dump: `") +
                             optargPtr + "'.  Try --dump help.");