diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-07 16:59:59 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-07 17:39:00 -0400 |
commit | d46b3638e09cd4e6f2c939386d686ed7ac2d8fdb (patch) | |
tree | c5318dd74f3045c19e1d14de30396671dd74bf0a /src/theory/arrays | |
parent | b702a70790f37e239c6f8c91bbc0ac107f1a4618 (diff) |
fix for nonterminating model-based array loop
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 1 |
1 files changed, 1 insertions, 0 deletions
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) { |