Fix some Win32 and SMT-LIB compliance bugs discovered by David Cok.

2 files changed, 7 insertions, 3 deletions

diff --git a/src/smt/options b/src/smt/options
index 05a138f60..458f42d6a 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -36,7 +36,7 @@ option produceAssignments produce-assignments --produce-assignments bool :defaul
 
 # This could go in src/main/options, but by SMT-LIBv2 spec, "interactive"
 # is a mode in which the assertion list must be kept.  So it belongs here.
-common-option interactive interactive-mode --interactive bool :read-write
+common-option interactive interactive-mode --interactive bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" :read-write
  force interactive mode
 
 option doITESimp --ite-simp bool :read-write
diff --git a/src/smt/smt_options_template.cpp b/src/smt/smt_options_template.cpp
index 4edd91a8d..987d2e3c7 100644
--- a/src/smt/smt_options_template.cpp
+++ b/src/smt/smt_options_template.cpp
@@ -62,11 +62,15 @@ void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value)
     throw OptionException("command-verbosity value must be a tuple (command-name, integer)");
   }
 
+  if(!value.isAtom()) {
+    throw OptionException("bad value for :" + key);
+  }
+
   string optionarg = value.getValue();
 
   ${smt_setoption_handlers}
 
-#line 70 "${template}"
+#line 74 "${template}"
 
   throw UnrecognizedOptionException(key);
 }
@@ -126,7 +130,7 @@ CVC4::SExpr SmtEngine::getOption(const std::string& key) const
 
   ${smt_getoption_handlers}
 
-#line 130 "${template}"
+#line 134 "${template}"
 
   throw UnrecognizedOptionException(key);
 }