diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index b9732c32e..6e6ee365a 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1768,7 +1768,7 @@ Expr SmtEngine::getValue(const Expr& e) theory::TheoryModel* m = d_theoryEngine->getModel(); Node resultNode; if( m ){ - resultNode = m->getValue( n ); + resultNode = Node::fromExpr( m->getValue( n.toExpr() ) ); } Trace("smt") << "--- got value " << n << " = " << resultNode << endl; // type-check the result we got @@ -1846,7 +1846,7 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) theory::TheoryModel* m = d_theoryEngine->getModel(); Node resultNode; if( m ){ - resultNode = m->getValue( n ); + resultNode = Node::fromExpr( m->getValue( n.toExpr() ) ); } // type-check the result we got |