From: Liana Hadarean <lianahady@gmail.com>
Date: Mon, 24 Aug 2015 10:46:07 +0000 (+0100)
Subject: Fix for bv core cardinality lemma generation
X-Git-Tag: cvc5-1.0.0~6252^2~8
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=531e7931a33079c4f1213ac56d285c578710ed49;p=cvc5.git

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 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));
             }