From a21f4e49f0ffac8b3857db9ad0154d7d17209b32 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 4 Jan 2022 13:04:53 -0600 Subject: [PATCH] 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. --- src/smt/process_assertions.cpp | 4 ---- 1 file changed, 4 deletions(-) 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); -- 2.30.2