summaryrefslogtreecommitdiff
path: root/src/prop/prop_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop/prop_engine.cpp')
-rw-r--r--src/prop/prop_engine.cpp6
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) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback