diff options
Diffstat (limited to 'src/smt/process_assertions.cpp')
| -rw-r--r-- | src/smt/process_assertions.cpp | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index 0bbc2eeae..6d6c81e3c 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -317,10 +317,7 @@ bool ProcessAssertions::apply(Assertions& as) { d_passes["ho-elim"]->apply(&assertions); } - - // rewrite equalities based on theory-specific rewriting - d_passes["theory-rewrite-eq"]->apply(&assertions); - + // begin: INVARIANT to maintain: no reordering of assertions or // introducing new ones @@ -332,6 +329,8 @@ bool ProcessAssertions::apply(Assertions& as) // ensure rewritten d_passes["rewrite"]->apply(&assertions); + // rewrite equalities based on theory-specific rewriting + d_passes["theory-rewrite-eq"]->apply(&assertions); // apply theory preprocess, which includes ITE removal d_passes["theory-preprocess"]->apply(&assertions); // This is needed because when solving incrementally, removeITEs may |