From c38f35164adc5ab255803765a568ef820fa8f3b2 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 28 Jul 2020 11:03:33 -0500 Subject: Use lemma property enum for OutputChannel::lemma (#4755) There are 3 Boolean flags for OutputChannel::lemma, and plans to add another for relevance. This makes them into a enum. --- src/theory/arrays/theory_arrays.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/theory/arrays') 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; -- cgit v1.2.3