diff options
Diffstat (limited to 'src/util/ite_removal.cpp')
-rw-r--r-- | src/util/ite_removal.cpp | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp index f26bbe0aa..7d4948251 100644 --- a/src/util/ite_removal.cpp +++ b/src/util/ite_removal.cpp @@ -30,7 +30,11 @@ void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap) { for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) { std::vector<Node> quantVar; - output[i] = run(output[i], output, iteSkolemMap, quantVar); + // Do this in two steps to avoid Node problems(?) + // Appears related to bug 512, splitting this into two lines + // fixes the bug on clang on Mac OS + Node itesRemoved = run(output[i], output, iteSkolemMap, quantVar); + output[i] = itesRemoved; } } |