From e1ac093478ef409707833ebe59be944536605c71 Mon Sep 17 00:00:00 2001
From: Peter Collingbourne <pcc@google.com>
Date: Sun, 16 Mar 2014 22:00:39 -0700
Subject: [PATCH] Fix for ite of >=64bit wide bitvectors with unconstrained
 condition.

---
 src/theory/unconstrained_simplifier.cpp | 35 ++++++++++++++-----------
 test/regress/regress0/Makefile.am       |  1 +
 test/regress/regress0/ite5.smt2         |  8 ++++++
 3 files changed, 28 insertions(+), 16 deletions(-)
 create mode 100644 test/regress/regress0/ite5.smt2

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 664958e5a..4ea78a826 100644
--- 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
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)
-- 
2.30.2