From ac7c25f879b222cadefca492102e277488df2bf2 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Wed, 1 Aug 2012 22:17:18 +0000
Subject: [PATCH] a couple fixes to SmtEngine::setOption().  thanks Andy for
 the report!

---
 src/smt/smt_engine.h             | 9 ++++++---
 src/smt/smt_options_template.cpp | 8 +++-----
 2 files changed, 9 insertions(+), 8 deletions(-)

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 53454b109..59f66521c 100644
--- 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 8c7fa1abf..f34a0e2db 100644
--- 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();
 }
-- 
2.30.2