diff options
Diffstat (limited to 'src/printer')
| -rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 2 | ||||
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 3 |
2 files changed, 2 insertions, 3 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 900651e1d..9ec522141 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -1185,7 +1185,7 @@ void DeclareFunctionCommandToStream(std::ostream& out, { out << tn; } - Node val = Node::fromExpr(model.getSmtEngine()->getValue(n.toExpr())); + Node val = model.getSmtEngine()->getValue(n); if (options::modelUninterpDtEnum() && val.getKind() == kind::STORE) { TypeNode type_node = val[1].getType(); diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 45cc2426c..7560b2ce4 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1455,8 +1455,7 @@ void Smt2Printer::toStream(std::ostream& out, // don't print out internal stuff return; } - Node val = - Node::fromExpr(theory_model->getSmtEngine()->getValue(n.toExpr())); + Node val = theory_model->getSmtEngine()->getValue(n); if (val.getKind() == kind::LAMBDA) { out << "(define-fun " << n << " " << val[0] << " " |