Merge pull request #21 from pcc/ite-fix

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

1 files changed, 19 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;