diff options
Diffstat (limited to 'src/smt/command.cpp')
| -rw-r--r-- | src/smt/command.cpp | 12 |
1 files changed, 2 insertions, 10 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp index ecd3c6f16..b1936d8cc 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1358,8 +1358,7 @@ void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) this->DefineFunctionCommand::invoke(smtEngine); if (!d_func.isNull() && d_func.getType().isBoolean()) { - smtEngine->addToAssignment( - d_func.getExprManager()->mkExpr(kind::APPLY, d_func)); + smtEngine->addToAssignment(d_func); } d_commandStatus = CommandSuccess::instance(); } @@ -1751,14 +1750,7 @@ void GetAssignmentCommand::invoke(SmtEngine* smtEngine) 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.first.toString())); v.emplace_back(SExpr::Keyword(p.second.toString())); sexprs.emplace_back(v); } |