Fix for bv core cardinality lemma generation

1 files changed, 5 insertions, 0 deletions

diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 13c31463b..9b8e0677e 100644
--- 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));
             }