Fix a serious bug in the preprocessor; problem inputs reported by Pantazis Deligiannis.

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 4fa8e53d8b2e9054db5021f14a10d40dddff7c00..0a9afab3c374796ad6f9a7fd09cb5eb242831d4d 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1970,8 +1970,7 @@ void SmtEnginePrivate::simpITE() {
 
   Trace("simplify") << "SmtEnginePrivate::simpITE()" << endl;
 
-  for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
-
+  for (unsigned i = 0; i < d_realAssertionsEnd; ++i) {
     d_assertionsToCheck[i] = d_smt.d_theoryEngine->ppSimpITE(d_assertionsToCheck[i]);
   }
 }