Fix for ite of >=64bit wide bitvectors with unconstrained condition.

diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp
index a6e885f975162c60ed396142bf12b752b3b27252..1157886396e5148b29439b51e72eccc244556e82 100644 (file)
--- a/src/theory/unconstrained_simplifier.cpp
+++ b/src/theory/unconstrained_simplifier.cpp
@@ -163,23 +163,26 @@ void UnconstrainedSimplifier::processUnconstrained()
               currentSub = Node();
             }
           }
-          else if (uCond && parent.getType().getCardinality().isFinite() && parent.getType().getCardinality().getFiniteCardinality() == 2) {
-            // Special case: condition is unconstrained, then and else are different, and total cardinality of the type is 2, then the result
-            // is unconstrained
-            Node test;
-            if (parent.getType().isBoolean()) {
-              test = Rewriter::rewrite(parent[1].iffNode(parent[2]));
-            }
-            else {
-              test = Rewriter::rewrite(parent[1].eqNode(parent[2]));
-            }
-            if (test == NodeManager::currentNM()->mkConst<bool>(false)) {
-              ++d_numUnconstrainedElim;
-              if (currentSub.isNull()) {
-                currentSub = current;
+          else if (uCond) {
+            Cardinality card = parent.getType().getCardinality();
+            if (card.isFinite() && !card.isLargeFinite() && card.getFiniteCardinality() == 2) {
+              // Special case: condition is unconstrained, then and else are different, and total cardinality of the type is 2, then the result
+              // is unconstrained
+              Node test;
+              if (parent.getType().isBoolean()) {
+                test = Rewriter::rewrite(parent[1].iffNode(parent[2]));
+              }
+              else {
+                test = Rewriter::rewrite(parent[1].eqNode(parent[2]));
+              }
+              if (test == NodeManager::currentNM()->mkConst<bool>(false)) {
+                ++d_numUnconstrainedElim;
+                if (currentSub.isNull()) {
+                  currentSub = current;
+                }
+                currentSub = newUnconstrainedVar(parent.getType(), currentSub);
+                current = parent;
               }
-              currentSub = newUnconstrainedVar(parent.getType(), currentSub);
-              current = parent;
             }
           }
           break;

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 664958e5a23e43a93c0653353714f01234654791..4ea78a82650bc34ec9288cf35540b4f588d0bde5 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -51,6 +51,7 @@ SMT2_TESTS = \
        ite2.smt2 \
        ite3.smt2 \
        ite4.smt2 \
+       ite5.smt2 \
        simple-lra.smt2 \
        simple-rdl.smt2 \
        simple-uf.smt2 \

diff --git a/test/regress/regress0/ite5.smt2 b/test/regress/regress0/ite5.smt2
new file mode 100644 (file)
index 0000000..e3d2bc9
--- /dev/null
+++ b/test/regress/regress0/ite5.smt2
@@ -0,0 +1,8 @@
+(set-logic QF_AUFBV )
+(set-info :status sat)
+(declare-fun arr0 () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun arr1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun arr2 () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(assert (bvult (ite (bvult (_ bv0 1) ((_ extract 0 0) (select arr1 (_ bv0 32)))) (concat (select arr0 (_ bv7 32)) (select arr0 (_ bv6 32)) (select arr0 (_ bv5 32)) (select arr0 (_ bv4 32)) (select arr0 (_ bv3 32)) (select arr0 (_ bv2 32)) (select arr0 (_ bv1 32)) (select arr0 (_ bv0 32))) (concat (_ bv0 57) ((_ extract 7 1) (select arr2 (_ bv0 32))))) (_ bv1 64) ))
+(check-sat)
+(exit)