diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2015-06-13 13:22:02 -0700 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2015-06-13 13:22:02 -0700 |
| commit | 4022c699dfbbd38105a4c59a4389c927f66770b7 (patch) | |
| tree | 6d79d1f31a1d0656f4d74ce1e843b84dfd5b51f6 | |
| parent | b3783ea06b286f343db135e1fa915d5c16107104 (diff) | |
Fixed bug in iteSimp
| -rw-r--r-- | src/theory/ite_utilities.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
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; } } |