Fix for bv core cardinality lemma generation

diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 13c31463bda1e35f22a52780fda3731754ff32a7..9b8e0677e53d9b2e008fa340f4b47844bfa3944f 100644 (file)
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -276,6 +276,11 @@ void CoreSolver::buildModel() {
           for (unsigned j = i + 1; j < representatives.size(); ++j) {
             TNode a = representatives[i];
             TNode b = representatives[j];
+            if (a.getKind() == kind::CONST_BITVECTOR &&
+                b.getKind() == kind::CONST_BITVECTOR) {
+              Assert (a != b);
+              continue;
+            }
             if (utils::getSize(a) == utils::getSize(b)) {
               equalities.push_back(utils::mkNode(kind::EQUAL, a, b));
             }