Remove spurious call to applySubs (#7871)

This call is preceded by another call to `apply-subs` at the beginning of preprocessing.

This is motivated by very large input benchmarks from Cetora where this preprocessing pass can take up to 5 seconds.

diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 8cfecda015135fcd8c4b273374c5fcc9bdafc887..329f426091f72ba110b76208684de0f8ab9fad27 100644 (file)
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -201,10 +201,6 @@ bool ProcessAssertions::apply(Assertions& as)
     applyPass("foreign-theory-rewrite", as);
   }
 
-  // Since this pass is not robust for the information tracking necessary for
-  // unsat cores, it's only applied if we are not doing unsat core computation
-  applyPass("apply-substs", as);
-
   // Assertions MUST BE guaranteed to be rewritten by this point
   applyPass("rewrite", as);