fixing bitvector bugs

* clauses shouldn't be erased when they could be a reason for outside propagation
* propagation of p and !p is ignored as this must lead to a conflict in the subtheory internally

1 files changed, 21 insertions, 0 deletions

diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index a8813b7aa..f8c763e3f 100644
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -30,6 +30,27 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
+enum SubTheory {
+  SUB_EQUALITY = 1,
+  SUB_BITBLAST = 2
+};
+
+inline std::ostream& operator << (std::ostream& out, SubTheory subtheory) {
+  switch (subtheory) {
+  case SUB_BITBLAST:
+    out << "BITBLASTER";
+    break;
+  case SUB_EQUALITY:
+    out << "EQUALITY";
+    break;
+  default:
+    Unreachable();
+    break;
+  }
+  return out;
+}
+
+
 const bool d_useEqualityEngine = true;
 const bool d_useSatPropagation = true;