diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-07-08 23:45:40 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-07-08 23:45:40 +0000 |
| commit | 4f964deb895010465e2bcc38da61e4cb06cb6cd6 (patch) | |
| tree | 651ad1ba8be1de2066b7bfc3895a7cb423916aaa /src/expr | |
| parent | d42f2360c109d22ae416f68aa3e4f5f7c6e14d20 (diff) | |
minor SMT-LIBv2 compliance issues
Diffstat (limited to 'src/expr')
| -rw-r--r-- | src/expr/command.cpp | 7 |
1 files changed, 6 insertions, 1 deletions
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&) { |