From cd98a21984d052a4f4702e6d2ce1718fa763c64b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 9 Apr 2020 14:01:34 -0700
Subject: [PATCH] decouple random update with assume eqs

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_lra.cpp | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 54bda5b64..92a27abd3 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1586,6 +1586,9 @@ public:
     }
 
     void random_update() {
+        if (m_use_nra_model || m_nla)
+            return;
+
         m_model_eqs.reset();
         svector<lpvar> vars;
         theory_var sz = static_cast<theory_var>(th.get_num_vars());
@@ -1625,7 +1628,7 @@ public:
                   }
               }
               tout << "\n"; );
-        if (!vars.empty() && !m_use_nra_model && !m_nla) {
+        if (!vars.empty()) {
             lp().random_update(vars.size(), vars.c_ptr());
         }
     }