diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-09-10 22:29:17 +0000 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-09-10 22:29:17 +0000 |
| commit | 680af6f4dc9e5d6616918e8fde18cd64774d0df5 (patch) | |
| tree | 5ec89cf302d5bc93ff1da80efa2125152d1c71b6 /src/smt | |
| parent | 586b07613702027fc685e55994e2a325961ca5b7 (diff) | |
modified getValue to return Expr instead of Node
Diffstat (limited to 'src/smt')
| -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 |