minor SMT-LIBv2 compliance issues

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 6d934c3fd6e79f09c2a51d8c26be9cd6145f60f3..8b7f1bfa4a81fab8060b4e1e2ab249c3555db5e3 100644 (file)
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -809,7 +809,9 @@ void GetAssertionsCommand::invoke(SmtEngine* smtEngine) throw() {
   try {
     stringstream ss;
     const vector<Expr> v = smtEngine->getAssertions();
+    ss << "(\n";
     copy( v.begin(), v.end(), ostream_iterator<Expr>(ss, "\n") );
+    ss << ")\n";
     d_result = ss.str();
     d_commandStatus = CommandSuccess::instance();
   } catch(exception& e) {
@@ -944,8 +946,11 @@ std::string GetInfoCommand::getFlag() const throw() {
 
 void GetInfoCommand::invoke(SmtEngine* smtEngine) throw() {
   try {
+    vector<SExpr> v;
+    v.push_back(SExpr(d_flag));
+    v.push_back(smtEngine->getInfo(d_flag));
     stringstream ss;
-    ss << smtEngine->getInfo(d_flag);
+    ss << SExpr(v);
     d_result = ss.str();
     d_commandStatus = CommandSuccess::instance();
   } catch(BadOptionException&) {

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ddc45228eb1b414840e614ce63a7dd8058c2ed43..08e335717c2bae99a751194ba05d7289021471a9 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -603,6 +603,9 @@ void SmtEngine::setLogicInternal() throw(AssertionException) {
 
 void SmtEngine::setInfo(const std::string& key, const SExpr& value)
   throw(BadOptionException, ModalException) {
+
+  NodeManagerScope nms(d_nodeManager);
+
   Trace("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl;
   if(Dump.isOn("benchmark")) {
     if(key == ":status") {
@@ -659,6 +662,9 @@ void SmtEngine::setInfo(const std::string& key, const SExpr& value)
 
 SExpr SmtEngine::getInfo(const std::string& key) const
   throw(BadOptionException) {
+
+  NodeManagerScope nms(d_nodeManager);
+
   Trace("smt") << "SMT getInfo(" << key << ")" << endl;
   if(key == ":all-statistics") {
     vector<SExpr> stats;