From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Fri, 14 Feb 2020 03:50:00 +0000 (-0300)
Subject: Forcing rewrite pass rather than asserting if formula has been rewritten (#3748)
X-Git-Tag: cvc5-1.0.0~3649
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d84d67018234bb6bb24dd9183a888892c3bfd4d7;p=cvc5.git

Forcing rewrite pass rather than asserting if formula has been rewritten (#3748)

This ensures that users or developers don't accidentally break the solver either via options or changing the SMT engine flow so that the formula is not rewritten up to a given point.
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 4a7c9def3..ad4d4e1d5 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3331,24 +3331,15 @@ void SmtEnginePrivate::processAssertions() {
     d_passes["bv-intro-pow2"]->apply(&d_assertions);
   }
 
-  if (options::unsatCores())
-  {
-    // special rewriting pass for unsat cores, since many of the passes below
-    // are skipped
-    d_passes["rewrite"]->apply(&d_assertions);
-  }
-  else
+  // 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
+  if (!options::unsatCores())
   {
     d_passes["apply-substs"]->apply(&d_assertions);
   }
 
-  // Assertions ARE guaranteed to be rewritten by this point
-#ifdef CVC4_ASSERTIONS
-  for (unsigned i = 0; i < d_assertions.size(); ++i)
-  {
-    Assert(Rewriter::rewrite(d_assertions[i]) == d_assertions[i]);
-  }
-#endif
+  // Assertions MUST BE guaranteed to be rewritten by this point
+  d_passes["rewrite"]->apply(&d_assertions);
 
   // Lift bit-vectors of size 1 to bool
   if (options::bitvectorToBool())