Make d_result in DE context dependent

(fixes bugs in bv, others with JH on)

2 files changed, 6 insertions, 4 deletions

diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index b1ecabf81..b38b3c1e0 100644
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -37,7 +37,7 @@ namespace CVC4 {
   d_satSolver(NULL),
   d_satContext(sc),
   d_userContext(uc),
-  d_result(SAT_VALUE_UNKNOWN)
+  d_result(sc, SAT_VALUE_UNKNOWN)
 {
   const Options* options = Options::current();
   Trace("decision") << "Creating decision engine" << std::endl;
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index fb6f673d9..e19307170 100644
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -50,10 +50,12 @@ class DecisionEngine {
 
   context::Context* d_satContext;
   context::Context* d_userContext;
-  SatValue d_result;
+
+  // Does decision engine know the answer?
+  context::CDO<SatValue> d_result;
 
   // Disable creating decision engine without required parameters
-  DecisionEngine() {}
+  DecisionEngine() : d_result(NULL) {}
 public:
   // Necessary functions
 
@@ -128,7 +130,7 @@ public:
 
   /** */
   Result getResult() {
-    switch(d_result) {
+    switch(d_result.get()) {
     case SAT_VALUE_TRUE: return Result(Result::SAT);
     case SAT_VALUE_FALSE: return Result(Result::UNSAT);
     case SAT_VALUE_UNKNOWN: return Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);