summaryrefslogtreecommitdiff
path: root/src/theory/ite_simplifier.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/ite_simplifier.cpp')
-rw-r--r--src/theory/ite_simplifier.cpp10
1 files changed, 2 insertions, 8 deletions
diff --git a/src/theory/ite_simplifier.cpp b/src/theory/ite_simplifier.cpp
index bf031fc94..ab8f159a9 100644
--- a/src/theory/ite_simplifier.cpp
+++ b/src/theory/ite_simplifier.cpp
@@ -447,10 +447,7 @@ Node ITESimplifier::simplifyWithCare(TNode e)
if (done) break;
Assert(v.getNumChildren() > 1);
- cs2 = getNewSet();
- cs2.getCareSet() = css;
- cs2.getCareSet().insert(v[1]);
- updateQueue(queue, v[0], cs2);
+ updateQueue(queue, v[0], cs);
cs2 = getNewSet();
cs2.getCareSet() = css;
cs2.getCareSet().insert(v[0]);
@@ -473,10 +470,7 @@ Node ITESimplifier::simplifyWithCare(TNode e)
if (done) break;
Assert(v.getNumChildren() > 1);
- cs2 = getNewSet();
- cs2.getCareSet() = css;
- cs2.getCareSet().insert(v[1].negate());
- updateQueue(queue, v[0], cs2);
+ updateQueue(queue, v[0], cs);
cs2 = getNewSet();
cs2.getCareSet() = css;
cs2.getCareSet().insert(v[0].negate());
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback