diff options
Diffstat (limited to 'src/smt/term_formula_removal.cpp')
| -rw-r--r-- | src/smt/term_formula_removal.cpp | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index 46135f12a..f3e0d0bd6 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -200,9 +200,11 @@ Node RemoveTermFormulas::runCurrent(std::pair<Node, uint32_t>& curr, // in the "non-variable Boolean term within term" case below. if (node.getKind() == kind::ITE && !nodeType.isBoolean()) { - // Here, we eliminate the ITE if we are not Boolean and if we do not contain - // a free variable. - if (!inQuant || !expr::hasFreeVar(node)) + // Here, we eliminate the ITE if we are not Boolean and if we are + // not in a quantified formula. This policy should be in sync with + // the policy for when to apply theory preprocessing to terms, see PR + // #5497. + if (!inQuant) { skolem = getSkolemForNode(node); if (skolem.isNull()) |