1 files changed, 47 insertions, 30 deletions

diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp
index 6a33adc56..d13cc1f03 100644
--- a/src/theory/unconstrained_simplifier.cpp
+++ b/src/theory/unconstrained_simplifier.cpp
@@ -79,7 +79,7 @@ void UnconstrainedSimplifier::visitAll(TNode assertion)
     d_visitedOnce[current] = parent;
 
     if (current.getNumChildren() == 0) {
-      if (current.isVar()) {
+      if (current.getKind()==kind::VARIABLE || current.getKind()==kind::SKOLEM) {
         d_unconstrained.insert(current);
       }
     }
@@ -563,39 +563,56 @@ void UnconstrainedSimplifier::processUnconstrained()
           }
           break;
 
-        // Bit-vector comparisons: replace with new Boolean variable, but have to also conjoin with a side condition
-        // as there is always one case when the comparison is forced to be false
+        // Bit-vector comparisons: replace with new Boolean variable, but have
+        // to also conjoin with a side condition as there is always one case
+        // when the comparison is forced to be false
         case kind::BITVECTOR_ULT:
-          strict = true;
         case kind::BITVECTOR_UGE:
-          goto bvineq;
-
         case kind::BITVECTOR_UGT:
-          strict = true;
         case kind::BITVECTOR_ULE:
-          swap = true;
-          goto bvineq;
-
         case kind::BITVECTOR_SLT:
-          strict = true;
         case kind::BITVECTOR_SGE:
-          isSigned = true;
-          goto bvineq;
-
         case kind::BITVECTOR_SGT:
-          strict = true;
-        case kind::BITVECTOR_SLE:
-          isSigned = true;
-          swap = true;
-
-        bvineq: {
+        case kind::BITVECTOR_SLE: {
+          // Tuples over (signed, swap, strict).
+          switch (parent.getKind()) {
+            case kind::BITVECTOR_UGE:
+              break;
+            case kind::BITVECTOR_ULT:
+              strict = true;
+              break;
+            case kind::BITVECTOR_ULE:
+              swap = true;
+              break;
+            case kind::BITVECTOR_UGT:
+              swap = true;
+              strict = true;
+              break;
+            case kind::BITVECTOR_SGE:
+              isSigned = true;
+              break;
+            case kind::BITVECTOR_SLT:
+              isSigned = true;
+              strict = true;
+              break;
+            case kind::BITVECTOR_SLE:
+              isSigned = true;
+              swap = true;
+              break;
+            case kind::BITVECTOR_SGT:
+              isSigned = true;
+              swap = true;
+              strict = true;
+              break;
+            default:
+              Unreachable();
+          }
           TNode other;
           bool left = false;
           if (parent[0] == current) {
             other = parent[1];
             left = true;
-          }
-          else {
+          } else {
             Assert(parent[1] == current);
             other = parent[0];
           }
@@ -608,14 +625,14 @@ void UnconstrainedSimplifier::processUnconstrained()
               }
               currentSub = newUnconstrainedVar(parent.getType(), currentSub);
               current = parent;
-            }
-            else {
+            } else {
               currentSub = Node();
             }
-          }
-          else {
+          } else {
             unsigned size = current.getType().getBitVectorSize();
-            BitVector bv = isSigned ? BitVector(size, Integer(1).multiplyByPow2(size - 1)) : BitVector(size, unsigned(0));
+            BitVector bv =
+                isSigned ? BitVector(size, Integer(1).multiplyByPow2(size - 1))
+                         : BitVector(size, unsigned(0));
             if (swap == left) {
               bv = ~bv;
             }
@@ -625,14 +642,14 @@ void UnconstrainedSimplifier::processUnconstrained()
             currentSub = newUnconstrainedVar(parent.getType(), currentSub);
             current = parent;
             NodeManager* nm = NodeManager::currentNM();
-            Node test = Rewriter::rewrite(other.eqNode(nm->mkConst<BitVector>(bv)));
+            Node test =
+                Rewriter::rewrite(other.eqNode(nm->mkConst<BitVector>(bv)));
             if (test == nm->mkConst<bool>(false)) {
               break;
             }
             if (strict) {
               currentSub = currentSub.andNode(test.notNode());
-            }
-            else {
+            } else {
               currentSub = currentSub.orNode(test);
             }
             // Delay adding this substitution - see comment at end of function