diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index c5cb34e8b..4feed6ddc 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2131,11 +2131,13 @@ public: switch (r) { case l_false: { m_stats.m_nla_lemmas += lv.size(); + int i = 0; for(const nla::lemma & l : lv) { m_lemma = l; //todo avoid the copy m_explanation = l.expl(); m_stats.m_nla_explanations += static_cast(l.expl().size()); false_case_of_check_nla(); + i++; } break; }