summaryrefslogtreecommitdiff
path: root/src/theory/arrays/theory_arrays.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arrays/theory_arrays.cpp')
-rw-r--r--src/theory/arrays/theory_arrays.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 37443c070..f008dc2a1 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -1522,7 +1522,7 @@ void TheoryArrays::check(Effort e) {
lemma = mkAnd(conjunctions, true);
// LSH FIXME: which kind of arrays lemma is this
Trace("arrays-lem") << "Arrays::addExtLemma " << lemma <<"\n";
- d_out->lemma(lemma, RULE_INVALID, false, false, true);
+ d_out->lemma(lemma, RULE_INVALID, LemmaProperty::SEND_ATOMS);
d_readTableContext->pop();
Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::check(): done" << endl;
return;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback