missed one case

diff --git a/src/theory/bv/equality_engine.h b/src/theory/bv/equality_engine.h
index 53c44bed0243bb4e7dbec2a4aaaac2b0dc3b7442..954253269cdc50462b89a4061736113be8935a58 100644 (file)
--- a/src/theory/bv/equality_engine.h
+++ b/src/theory/bv/equality_engine.h
@@ -321,7 +321,8 @@ public:
   inline bool hasTerm(TNode t) const;
 
   /**
-   * Adds an equality t1 = t2 to the database. Returns false if any of the triggers failed.
+   * Adds an equality t1 = t2 to the database. Returns false if any of the triggers failed, or a
+   * conflict was introduced.
    */
   bool addEquality(TNode t1, TNode t2, Node reason);
 
@@ -437,6 +438,13 @@ bool EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::addEquality(
   // If already the same, we're done
   if (t1classId == t2classId) return true;
 
+  // Check for constants
+  if (d_nodes[t1classId].getMetaKind() == kind::metakind::CONSTANT &&
+      d_nodes[t2classId].getMetaKind() == kind::metakind::CONSTANT) {
+    d_notify.conflict(reason);
+    return false;
+  }
+
   // Get the nodes of the representatives
   EqualityNode& node1 = getEqualityNode(t1classId);
   EqualityNode& node2 = getEqualityNode(t2classId);

diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index fa9762cb738271c108e52300fda7d9230b2475e8..8eaa332ebc34b84a6df8b7d8f7df5a1813b8902f 100644 (file)
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -44,6 +44,9 @@ public:
     bool operator () (size_t triggerId) {
       return d_theoryBV.triggerEquality(triggerId);
     }
+    void conflict(Node explanation) {
+      d_theoryBV.d_out->conflict(explanation);
+    }
   };
 
   struct BVEqualitySettings {

diff --git a/test/regress/regress0/bv/core/Makefile.am b/test/regress/regress0/bv/core/Makefile.am
index 947dc65ad044e3b064efebc644c205a5bbf41d64..0e559f6f237b9e9b34f6b706fe1d6105559a07b4 100644 (file)
--- a/test/regress/regress0/bv/core/Makefile.am
+++ b/test/regress/regress0/bv/core/Makefile.am
@@ -41,6 +41,7 @@ TESTS =       \
        equality-00.smt \
        equality-01.smt \
        equality-02.smt \
+  equality-05.smt \
        bv_eq_diamond10.smt \
        slice-01.smt \
        slice-02.smt \

diff --git a/test/regress/regress0/bv/core/equality-05.cvc b/test/regress/regress0/bv/core/equality-05.cvc
new file mode 100644 (file)
index 0000000..93bef50
--- /dev/null
+++ b/test/regress/regress0/bv/core/equality-05.cvc
@@ -0,0 +1,6 @@
+x,y:BITVECTOR(1);
+ASSERT(x = 0bin0);
+ASSERT(y = 0bin1);
+ASSERT(x = y);
+CHECKSAT;
+

diff --git a/test/regress/regress0/bv/core/equality-05.smt b/test/regress/regress0/bv/core/equality-05.smt
new file mode 100644 (file)
index 0000000..a7b9f61
--- /dev/null
+++ b/test/regress/regress0/bv/core/equality-05.smt
@@ -0,0 +1,11 @@
+(benchmark equality
+  :status unsat
+  :logic QF_BV
+  :extrafuns ((x BitVec[1]))
+  :extrafuns ((y BitVec[1]))
+  :assumption (= x bv0[1])
+  :assumption (= y bv1[1])
+  :assumption (= x y)
+  :formula
+true
+)

diff --git a/test/regress/regress0/bv/core/slice-20.smt b/test/regress/regress0/bv/core/slice-20.smt
new file mode 100644 (file)
index 0000000..66fac57
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-20.smt
@@ -0,0 +1,16 @@
+(benchmark slice
+  :status unsat
+  :logic QF_BV
+  :extrafuns ((x1 BitVec[4]))
+  :extrafuns ((y1 BitVec[4]))
+  :extrafuns ((x2 BitVec[2]))
+  :extrafuns ((y2 BitVec[2]))
+  :extrafuns ((x3 BitVec[1]))
+  :extrafuns ((y3 BitVec[1]))
+  :assumption (= x1 y1)
+  :assumption (= x1 (concat x2 x2))
+  :assumption (= x2 (concat x3 x3))
+  :assumption (= y1 (concat y2 y2))
+  :assumption (= y2 (concat y3 y3))
+  :formula (not (= x3 y3))
+)