SmtEngine::getAssignment now returns a vector of assignments. (#1628)

1 files changed, 17 insertions, 1 deletions

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 25479a20b..040d87250 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1321,7 +1321,23 @@ void GetAssignmentCommand::invoke(SmtEngine* smtEngine)
 {
   try
   {
-    d_result = smtEngine->getAssignment();
+    std::vector<std::pair<Expr,Expr>> assignments  = smtEngine->getAssignment();
+    vector<SExpr> sexprs;
+    for (const auto& p : assignments)
+    {
+      vector<SExpr> v;
+      if (p.first.getKind() == kind::APPLY)
+      {
+        v.emplace_back(SExpr::Keyword(p.first.getOperator().toString()));
+      }
+      else
+      {
+        v.emplace_back(SExpr::Keyword(p.first.toString()));
+      }
+      v.emplace_back(SExpr::Keyword(p.second.toString()));
+      sexprs.emplace_back(v);
+    }
+    d_result = SExpr(sexprs);
     d_commandStatus = CommandSuccess::instance();
   }
   catch (RecoverableModalException& e)