diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 74df2c20d..4508511b1 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2199,11 +2199,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; }