From: Morgan Deters <mdeters@gmail.com>
Date: Sun, 8 Jul 2012 23:45:40 +0000 (+0000)
Subject: minor SMT-LIBv2 compliance issues
X-Git-Tag: cvc5-1.0.0~7943
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4f964deb895010465e2bcc38da61e4cb06cb6cd6;p=cvc5.git

minor SMT-LIBv2 compliance issues
---

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 6d934c3fd..8b7f1bfa4 100644
--- 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 ddc45228e..08e335717 100644
--- 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;