From 84933c443506135c5d8d9c20269a09bbaac8eb22 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Fri, 14 Feb 2020 16:06:57 -0800
Subject: [PATCH] relax the literal check in theory_lra

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/smt/theory_lra.cpp | 2 ++
 1 file changed, 2 insertions(+)

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<unsigned>(l.expl().size());
                 false_case_of_check_nla();
+                i++;
             }
             break;
         }