diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-17 02:29:14 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-17 02:29:14 +0000 |
commit | 9f875caa97a4943ed5d56f6472745828e197909d (patch) | |
tree | 1cea288c623bf1d3a281113d0e1e78011a09601a /src | |
parent | edaf5ab57434d5d9a081c4925b96503d203f9de9 (diff) |
Removed assertion that can fail
Diffstat (limited to 'src')
-rw-r--r-- | src/smt/smt_engine.cpp | 18 |
1 files 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; |