diff options
Diffstat (limited to 'src/smt/process_assertions.cpp')
| -rw-r--r-- | src/smt/process_assertions.cpp | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index 77c7d450e..8b9b0a53c 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -328,13 +328,8 @@ bool ProcessAssertions::apply(Assertions& as) // ensure rewritten d_passes["rewrite"]->apply(&assertions); - // apply theory preprocess + // apply theory preprocess, which includes ITE removal d_passes["theory-preprocess"]->apply(&assertions); - // Must remove ITEs again since theory preprocessing may introduce them. - // Notice that we alternatively could ensure that the theory-preprocess - // pass above calls TheoryPreprocess::preprocess instead of - // TheoryPreprocess::theoryPreprocess, as the former also does ITE removal. - d_passes["ite-removal"]->apply(&assertions); // This is needed because when solving incrementally, removeITEs may // introduce skolems that were solved for earlier and thus appear in the // substitution map. |