From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 4 Jan 2022 19:04:53 +0000 (-0600)
Subject: Remove spurious call to applySubs (#7871)
X-Git-Tag: cvc5-1.0.0~605
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a21f4e49f0ffac8b3857db9ad0154d7d17209b32;p=cvc5.git

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 8cfecda01..329f42609 100644
--- 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);