a couple fixes to SmtEngine::setOption(). thanks Andy for the report!

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 53454b109e5261afd126e8f2b1a32e10c5857f7c..59f66521c1ccf2646cb78e9f883e8327cf133e42 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -554,11 +554,14 @@ public:
   /**
    * Used as a predicate for options preprocessor.
    */
-  static void beforeSearch(std::string option, bool value, SmtEngine* smt) {
-    if(smt != NULL && (smt->d_queryMade || smt->d_problemExtended)) {
+  static void beforeSearch(std::string option, bool value, SmtEngine* smt) throw(ModalException) {
+    // FIXME: should be the following test...
+    // if(smt != NULL && (smt->d_queryMade || smt->d_problemExtended)) {
+    // ...but addToModelType() etc. make a stronger assumption:
+    if(smt != NULL && smt->d_fullyInited) {
       std::stringstream ss;
       ss << "cannot change option `" << option << "' after assertions have been made";
-      throw OptionException(ss.str());
+      throw ModalException(ss.str());
     }
   }
 

diff --git a/src/smt/smt_options_template.cpp b/src/smt/smt_options_template.cpp
index 8c7fa1abf97717056b1e7b18e14892ed8b8536f8..f34a0e2dbf208fa40a82668628c72782001db650 100644 (file)
--- a/src/smt/smt_options_template.cpp
+++ b/src/smt/smt_options_template.cpp
@@ -47,13 +47,11 @@ void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value)
     Dump("benchmark") << SetOptionCommand(key, value);
   }
 
-  stringstream ss;
-  ss << value;
-  string optarg = ss.str();
+  string optarg = value.getValue();
 
   ${smt_setoption_handlers}
 
-#line 57 "${template}"
+#line 55 "${template}"
 
   throw BadOptionException();
 }
@@ -70,7 +68,7 @@ CVC4::SExpr SmtEngine::getOption(const std::string& key) const
 
   ${smt_getoption_handlers}
 
-#line 74 "${template}"
+#line 72 "${template}"
 
   throw BadOptionException();
 }