fix for nonterminating model-based array loop

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index c465ed97a44d5618b1f7b9ecc1a102bb99faa86c..5d6356a5bdac3f272baa7385c632473a6984fe40 100644 (file)
--- 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 732f89e6610592f161d1740fc999cdff6acb8caf..3e0a41591444c770715098e0b1c4bef699020fc9 100644 (file)
--- 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 3aa3a1ec5a98889118fb1983848721ac64e1ba0d..97b018214a6d590b329f576a47513ca4560dcec1 100644 (file)
--- 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 );
     }