Fixes to Valuation.

2 files changed, 12 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) {
diff --git a/src/prop/sat.h b/src/prop/sat.h
index 88df366e2..f9e135c0d 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -232,8 +232,12 @@ public:
 
   void setCnfStream(CnfStream* cnfStream);
 
+  /** Call value() during the search.*/
   SatLiteralValue value(SatLiteral l);
 
+  /** Call value() when the search is done.*/
+  SatLiteralValue modelValue(SatLiteral l);
+
   int getLevel() const;
 
   void push();
@@ -294,6 +298,10 @@ inline SatVariable SatSolver::newVar(bool theoryAtom) {
 }
 
 inline SatLiteralValue SatSolver::value(SatLiteral l) {
+  return d_minisat->value(l);
+}
+
+inline SatLiteralValue SatSolver::modelValue(SatLiteral l) {
   return d_minisat->modelValue(l);
 }