From e0ea9a22721a332be2a2354846ffdf5f72c6a6de Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.nyu.edu>
Date: Thu, 31 May 2012 17:15:02 +0000
Subject: [PATCH] Fixed bug in bv: one more case where non-shared equality was
 getting propagated Added a global push and pop around solving - fixes an
 assertion failure when TNodes are still around in a CDHashMap at destruction
 time.

---
 src/smt/smt_engine.cpp      |  4 ++++
 src/theory/bv/theory_bv.cpp | 33 +++++++++++++++++++++++----------
 2 files changed, 27 insertions(+), 10 deletions(-)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0d3a220c9..64e3e4ae4 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -293,6 +293,8 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   d_theoryEngine->setDecisionEngine(d_decisionEngine);
   // d_decisionEngine->setPropEngine(d_propEngine);
 
+  d_context->push();
+
   d_definedFunctions = new(true) DefinedFunctionMap(d_userContext);
 
   // [MGD 10/20/2011] keep around in incremental mode, due to a
@@ -349,6 +351,8 @@ SmtEngine::~SmtEngine() throw() {
 
     shutdown();
 
+    d_context->pop();
+
     if(d_assignments != NULL) {
       d_assignments->deleteSelf();
     }
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 79ab955aa..251650bf2 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -148,12 +148,13 @@ void TheoryBV::propagate(Effort e) {
     Node normalized = Rewriter::rewrite(literal);
 
     TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;  
-    // check if it's a shared equality in the current context
-    if (atom.getKind() != kind::EQUAL || d_valuation.isSatLiteral(normalized) ||
-        (d_sharedTermsSet.find(atom[0]) != d_sharedTermsSet.end() &&
-         d_sharedTermsSet.find(atom[1]) != d_sharedTermsSet.end())) {
-    
-      bool satValue;
+    bool isSharedLiteral = (atom.getKind() == kind::EQUAL &&
+                            (d_sharedTermsSet.find(atom[0]) != d_sharedTermsSet.end() &&
+                             d_sharedTermsSet.find(atom[1]) != d_sharedTermsSet.end()));
+
+    // Check if this is a SAT literal
+    if (d_valuation.isSatLiteral(normalized)) {
+      bool satValue = false;
       if (!d_valuation.hasSatValue(normalized, satValue) || satValue) {
         // check if we already propagated the negation
         Node negLiteral = literal.getKind() == kind::NOT ? (Node)literal[0] : mkNot(literal);
@@ -166,11 +167,16 @@ void TheoryBV::propagate(Effort e) {
           setConflict(mkAnd(assumptions)); 
           return;
         }
-        
-        BVDebug("bitvector") << indent() << "TheoryBV::propagate(): " << literal << std::endl;
-        d_out->propagate(literal);
-        d_alreadyPropagatedSet.insert(literal); 
+        // If it's not a shared literal and hasn't already been set to true, we propagate the normalized version
+        // shared literals are handled below
+        if (!isSharedLiteral && !satValue) {
+          BVDebug("bitvector") << indent() << "TheoryBV::propagate(): " << normalized << std::endl;
+          d_out->propagate(normalized);
+          d_alreadyPropagatedSet.insert(normalized); 
+          return;
+        }
       } else {
+        // 
         Debug("bitvector") << indent() << "TheoryBV::propagate(): in conflict, normalized = " << normalized << std::endl;
         Node negatedLiteral;
         std::vector<TNode> assumptions;
@@ -181,9 +187,16 @@ void TheoryBV::propagate(Effort e) {
         return;
       }
     }
+    // Either it was not a SAT literal or it was but it is also shared - in that case we have to propagate the original literal (not the normalized one)
+    if (isSharedLiteral) {
+      BVDebug("bitvector") << indent() << "TheoryBV::propagate(): " << literal << std::endl;
+      d_out->propagate(literal);
+      d_alreadyPropagatedSet.insert(literal); 
+    }
   }
 }
 
+
 Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
   switch(in.getKind()) {
   case kind::EQUAL:
-- 
2.30.2