From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 8 Aug 2013 23:29:50 +0000 (-0400)
Subject: Fix a serious bug in the preprocessor; problem inputs reported by Pantazis Deligiannis.
X-Git-Tag: cvc5-1.0.0~7287^2~40
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=663c2df0d089b316254bb713078dee8889129609;p=cvc5.git

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 4fa8e53d8..0a9afab3c 100644
--- 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]);
   }
 }