From: Clark Barrett <barrett@cs.nyu.edu>
Date: Sat, 13 Jun 2015 20:23:07 +0000 (-0700)
Subject: Fixed bug in iteSimp
X-Git-Tag: cvc5-1.0.0~6281
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b66afc0f672c46c9705284459674efc5a857106a;p=cvc5.git

Fixed bug in iteSimp
---

diff --git a/src/theory/ite_utilities.cpp b/src/theory/ite_utilities.cpp
index dcb75a44a..20464b14e 100644
--- 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;
   }
 }