Fix infinite loop in --bitblast-aig/--bv-aig-simp options.

1 files changed, 15 insertions, 1 deletions

diff --git a/src/theory/bv/options_handlers.h b/src/theory/bv/options_handlers.h
index c917aa9dd..a7a7101d2 100644
--- a/src/theory/bv/options_handlers.h
+++ b/src/theory/bv/options_handlers.h
@@ -46,7 +46,6 @@ inline void abcEnabledBuild(std::string option, std::string value, SmtEngine* sm
 #endif /* CVC4_USE_ABC */
 }
 
-
 static const std::string bitblastingModeHelp = "\
 Bit-blasting modes currently supported by the --bitblast option:\n\
 \n\
@@ -139,6 +138,21 @@ inline BvSlicerMode stringToBvSlicerMode(std::string option, std::string optarg,
   }
 }
 
+inline void setBitblastAig(std::string option, bool arg, SmtEngine* smt) throw(OptionException) {
+  if(arg) {
+    if(options::bitblastMode.wasSetByUser()) {
+      if(options::bitblastMode() != BITBLAST_MODE_EAGER) {
+        throw OptionException("bitblast-aig must be used with eager bitblaster");
+      }
+    } else {
+      options::bitblastMode.set(stringToBitblastMode("", "eager", smt));
+    }
+    if(!options::bitvectorAigSimplifications.wasSetByUser()) {
+      options::bitvectorAigSimplifications.set("balance;drw");
+    }
+  }
+}
+
 }/* CVC4::theory::bv namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */