diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2013-03-27 22:43:18 -0400 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2013-03-27 22:43:18 -0400 |
commit | 3242df3ac7fba2393659cdccd1579084e6a8e59a (patch) | |
tree | 60c0e05496c3f8db431777bb5601612be4f2ccda /src | |
parent | a5c5c2f8db7340ceaa3628575ff0e672370374cc (diff) |
Fixed bug in arrays
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 62de6092b..02575edd4 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -1141,6 +1141,19 @@ void TheoryArrays::checkModel(Effort e) d_decisions.pop_back(); if (all.find(decision) != all.end()) { if (getSatContext()->getLevel() < baseLevel) { + if (all.size() == 1) { + d_lemmas.push_back(decision.negate()); + } + else { + NodeBuilder<> disjunction(kind::OR); + std::set<TNode>::const_iterator it = all.begin(); + std::set<TNode>::const_iterator it_end = all.end(); + while (it != it_end) { + disjunction << (*it).negate(); + ++it; + } + d_lemmas.push_back(disjunction); + } goto finish; } all.erase(decision); |