From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Sun, 20 Mar 2011 01:41:48 +0000 (+0000)
Subject: missed one case
X-Git-Tag: cvc5-1.0.0~8643
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3af0d6493cdea4be4130076fee93ebbeff669545;p=cvc5.git

missed one case
---

diff --git a/src/theory/bv/equality_engine.h b/src/theory/bv/equality_engine.h
index 53c44bed0..954253269 100644
--- 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 fa9762cb7..8eaa332eb 100644
--- 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 947dc65ad..0e559f6f2 100644
--- 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
index 000000000..93bef502d
--- /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
index 000000000..a7b9f6185
--- /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
index 000000000..66fac573b
--- /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))
+)