From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Fri, 6 Apr 2012 19:01:25 +0000 (+0000)
Subject: processing assertions in bit-vectors even when in fullcheck (needed for sharing)
X-Git-Tag: cvc5-1.0.0~8238
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bc63c26f48851a79d21139f32f2c57daeb47f49d;p=cvc5.git

processing assertions in bit-vectors even when in fullcheck (needed for sharing)
---

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index e8e1aead6..429e5ff19 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -73,24 +73,22 @@ void TheoryBV::preRegisterTerm(TNode node) {
 }
 
 void TheoryBV::check(Effort e) {
-  if (e == EFFORT_STANDARD) {
-    BVDebug("bitvector") << "TheoryBV::check " << e << "\n"; 
-    BVDebug("bitvector")<< "TheoryBV::check(" << e << ")" << std::endl;
-    while (!done()) {
-      TNode assertion = get();
-      // make sure we do not assert things we propagated 
-      if (!hasBeenPropagated(assertion)) {
-        BVDebug("bitvector-assertions") << "TheoryBV::check assertion " << assertion << "\n"; 
-        bool ok = d_bitblaster->assertToSat(assertion, true);
-        if (!ok) {
-          std::vector<TNode> conflictAtoms;
-          d_bitblaster->getConflict(conflictAtoms);
-          d_statistics.d_avgConflictSize.addEntry(conflictAtoms.size());
-          Node conflict = mkConjunction(conflictAtoms);
-          d_out->conflict(conflict);
-          BVDebug("bitvector") << "TheoryBV::check returns conflict: " <<conflict <<" \n ";
-          return;
-        }
+  BVDebug("bitvector") << "TheoryBV::check " << e << "\n";
+  BVDebug("bitvector")<< "TheoryBV::check(" << e << ")" << std::endl;
+  while (!done()) {
+    TNode assertion = get();
+    // make sure we do not assert things we propagated
+    if (!hasBeenPropagated(assertion)) {
+      BVDebug("bitvector-assertions") << "TheoryBV::check assertion " << assertion << "\n";
+      bool ok = d_bitblaster->assertToSat(assertion, true);
+      if (!ok) {
+        std::vector<TNode> conflictAtoms;
+        d_bitblaster->getConflict(conflictAtoms);
+        d_statistics.d_avgConflictSize.addEntry(conflictAtoms.size());
+        Node conflict = mkConjunction(conflictAtoms);
+        d_out->conflict(conflict);
+        BVDebug("bitvector") << "TheoryBV::check returns conflict: " <<conflict <<" \n ";
+        return;
       }
     }
   }