From 21c626e3eebc100e78e7e27bf0ad5f1d603bbae8 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 24 Dec 2020 03:22:43 -0800
Subject: [PATCH] fix bound miss-computation, include sporadic nra check for
 #4913

---
 src/math/lp/nla_core.cpp | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index e31bd02fb9b..eba1694b16e 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1470,7 +1470,7 @@ void core::check_weighted(unsigned sz, std::pair<unsigned, std::function<void(vo
             if (n < checks[i].first) {
                 seen.insert(i);
                 checks[i].second();
-                bound -= n;
+                bound -= checks[i].first;
                 break;
             }
             n -= checks[i].first;
@@ -1523,9 +1523,14 @@ lbool core::check(vector<lemma>& l_vec) {
               { 2, check2 }, 
               { 1, check3 }};
         check_weighted(3, checks);
+
+        if (!conflict_found() && m_nla_settings.run_nra() && random() % 30 == 0) {
+            ret = m_nra.check();
+            m_stats.m_nra_calls++;
+        }
     }
 
-    if (l_vec.empty() && !done() && m_nla_settings.run_nra()) {
+    if (l_vec.empty() && !done() && m_nla_settings.run_nra() && ret == l_undef) {
         ret = m_nra.check();
         m_stats.m_nra_calls++;
     }