Merge branch 'master' of https://github.com/CVC4/CVC4

5 files changed, 38 insertions, 16 deletions

diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp
index a6e885f97..115788639 100644
--- 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 5df8577af..f16e18bdf 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -53,6 +53,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
index 000000000..e3d2bc9b8
--- /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)
diff --git a/test/regress/regress0/unconstrained/Makefile.am b/test/regress/regress0/unconstrained/Makefile.am
index fcae3196a..dcc44d43a 100644
--- a/test/regress/regress0/unconstrained/Makefile.am
+++ b/test/regress/regress0/unconstrained/Makefile.am
@@ -65,6 +65,7 @@ TESTS =	\
 	bvult.smt2 \
 	geq.smt2 \
 	gt.smt2 \
+	ite.smt2 \
 	leq.smt2 \
 	lt.smt2 \
 	uf1.smt2 \
diff --git a/test/regress/regress0/unconstrained/ite.smt2 b/test/regress/regress0/unconstrained/ite.smt2
new file mode 100644
index 000000000..4dc1cc295
--- /dev/null
+++ b/test/regress/regress0/unconstrained/ite.smt2
@@ -0,0 +1,9 @@
+(set-logic QF_AUFBV )
+(set-info :status sat)
+(declare-sort U 0)
+(declare-fun a () (Array U (_ BitVec 64) ) )
+(declare-fun i () U)
+(declare-fun p () Bool)
+(assert (= (_ bv0 64) (ite p (select a i) (_ bv1 64))))
+(check-sat)
+(exit)