Fixes to Valuation.

1 files changed, 8 insertions, 0 deletions

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);
 }