Fixed bug in iteSimp

diff --git a/src/theory/ite_utilities.cpp b/src/theory/ite_utilities.cpp
index dcb75a44af191de0c3de73e913f54694e1bb284d..20464b14e42efe57ab47aab9d9a832ceae5a2ba0 100644 (file)
--- a/src/theory/ite_utilities.cpp
+++ b/src/theory/ite_utilities.cpp
@@ -1028,7 +1028,7 @@ Node ITESimplifier::intersectConstantIte(TNode lcite, TNode rcite){
       Node bothHold = lefteq.andNode(righteq);
       nb << bothHold;
     }
-    Node result = (nb.getNumChildren() >= 1) ? (Node)nb : nb[0];
+    Node result = (nb.getNumChildren() > 1) ? (Node)nb : nb[0];
     return result;
   }
 }