fix for nonterminating model-based array loop

3 files changed, 6 insertions, 1 deletions

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index c465ed97a..5d6356a5b 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -280,6 +280,7 @@ void PropEngine::interrupt() throw(ModalException) {
 
 void PropEngine::spendResource() throw() {
   // TODO implement me
+  checkTime();
 }
 
 bool PropEngine::properExplanation(TNode node, TNode expl) const {
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 732f89e66..3e0a41591 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -1067,6 +1067,7 @@ void TheoryArrays::checkModel(Effort e)
   int numrestarts = 0;
   while (true || numrestarts < 1 || fullEffort(e) || combination(e)) {
     ++numrestarts;
+    d_out->safePoint();
     int level = getSatContext()->getLevel();
     d_getModelValCache.clear();
     for (constraintIdx = 0; constraintIdx < d_modelConstraints.size(); ++constraintIdx) {
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 3aa3a1ec5..97b018214 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -275,8 +275,10 @@ class TheoryEngine {
     }
 
     void safePoint() throw(theory::Interrupted, AssertionException) {
-      if (d_engine->d_interrupted)
+      spendResource();
+      if (d_engine->d_interrupted) {
         throw theory::Interrupted();
+      }
     }
 
     void conflict(TNode conflictNode) throw(AssertionException) {
@@ -340,6 +342,7 @@ class TheoryEngine {
     void spendResource() throw() {
       d_engine->spendResource();
     }
+
     void handleUserAttribute( const char* attr, theory::Theory* t ){
       d_engine->handleUserAttribute( attr, t );
     }