Updates to theory preprocess equality (#5776)

This makes 3 changes related to arithmetic preprocessing of equalities which revert to the original behavior of master before a129c57.

For background, the commit a129c57 unintentionally changed the default behavior slightly in 3 ways (each corrected in this PR), which led a performance regression on QF_LIA in current master.

The 3 fixes are:
(1) Rewrite equalities should be applied as a post-rewrite, not a pre-rewrite in the theory-rewrite-eq preprocessing pass. This is particularly important for equalities between ITE terms that contain other equalities recursively.
(2) theory-rewrite-eq should apply after rewriting and just before the normal theory preprocessing.
(3) The arith-brab test should call ppRewrite on the arithmetic equality it introduces, as it has a choice of whether to eliminate the equality before the lemma is sent out.

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