diff options
Diffstat (limited to 'src/prop/prop_engine.cpp')
-rw-r--r-- | src/prop/prop_engine.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index d64aadc96..44709630d 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -104,7 +104,7 @@ void PropEngine::printSatisfyingAssignment(){ SatLiteral l = curr.second.literal; if(!sign(l)) { Node n = curr.first; - SatLiteralValue value = d_satSolver->value(l); + SatLiteralValue value = d_satSolver->modelValue(l); Debug("prop-value") << "'" << l << "' " << value << " " << n << endl; } } @@ -138,7 +138,9 @@ Result PropEngine::checkSat() { Node PropEngine::getValue(TNode node) { Assert(node.getType().isBoolean()); - SatLiteralValue v = d_satSolver->value(d_cnfStream->getLiteral(node)); + SatLiteral lit = d_cnfStream->getLiteral(node); + + SatLiteralValue v = d_satSolver->value(lit); if(v == l_True) { return NodeManager::currentNM()->mkConst(true); } else if(v == l_False) { |