From 9f875caa97a4943ed5d56f6472745828e197909d Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Sun, 17 Jun 2012 02:29:14 +0000 Subject: [PATCH] Removed assertion that can fail --- src/smt/smt_engine.cpp | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 5e8d71198..e1d247521 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1446,12 +1446,6 @@ void SmtEnginePrivate::processAssertions() { d_smt.d_numAssertionsPost += d_assertionsToCheck.size(); } - // begin: INVARIANT to maintain: no reordering of assertions or - // introducing new ones -#ifdef CVC4_ASSERTIONS - unsigned iteRewriteAssertionsEnd = d_assertionsToCheck.size(); -#endif - if(Options::current()->repeatSimp) { d_assertionsToCheck.swap(d_assertionsToPreprocess); noConflict &= simplifyAssertions(); @@ -1471,12 +1465,20 @@ void SmtEnginePrivate::processAssertions() { if(builder.getNumChildren() > 1) { d_assertionsToCheck[d_realAssertionsEnd-1] = Rewriter::rewrite(Node(builder)); } - // TODO: remove this - need to double-check it's not needed + // For some reason this is needed for some benchmarks, such as + // http://church.cims.nyu.edu/benchmarks/smtlib2/QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2 + // Figure it out later removeITEs(); - Assert(iteRewriteAssertionsEnd == d_assertionsToCheck.size()); + // Assert(iteRewriteAssertionsEnd == d_assertionsToCheck.size()); } } + // begin: INVARIANT to maintain: no reordering of assertions or + // introducing new ones +#ifdef CVC4_ASSERTIONS + unsigned iteRewriteAssertionsEnd = d_assertionsToCheck.size(); +#endif + Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; -- 2.30.2