From 7a04e52c41c9837a95bc958b008b1599d7e15b97 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 26 Mar 2020 16:22:24 -0700
Subject: [PATCH] fix ordering of delayed assume eqs

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_arith.h     |  1 +
 src/smt/theory_arith_aux.h |  2 +-
 src/smt/theory_arith_pp.h  |  1 +
 src/smt/theory_lra.cpp     | 15 +++++++--------
 4 files changed, 10 insertions(+), 9 deletions(-)

diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index 5ea615ab4..bc0c5191f 100644
--- a/src/smt/theory_arith.h
+++ b/src/smt/theory_arith.h
@@ -46,6 +46,7 @@ namespace smt {
         unsigned m_assert_lower, m_assert_upper, m_assert_diseq, m_core2th_eqs, m_core2th_diseqs;
         unsigned m_th2core_eqs, m_th2core_diseqs, m_bound_props, m_offset_eqs, m_fixed_eqs, m_offline_eqs;
         unsigned m_max_min; 
+        unsigned m_assume_eqs;
         unsigned m_gb_simplify, m_gb_superpose, m_gb_compute_basis, m_gb_num_processed;
         unsigned m_nl_branching, m_nl_linear, m_nl_bounds, m_nl_cross_nested;
         unsigned m_branch_infeasible_int, m_branch_infeasible_var;
diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index 6c9016b2a..aae4b99be 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -2237,7 +2237,6 @@ namespace smt {
         if (result)
             get_context().push_trail(restore_size_trail<context, std::pair<theory_var, theory_var>, false>(m_assume_eq_candidates, old_sz));
         return delayed_assume_eqs();
-        // return this->assume_eqs(m_var_value_table);
     }
 
     template<typename Ext>
@@ -2258,6 +2257,7 @@ namespace smt {
             if (get_value(v1) == get_value(v2) && 
                 get_enode(v1)->get_root() != get_enode(v2)->get_root() &&
                 assume_eq(get_enode(v1), get_enode(v2))) {
+                ++m_stats.m_assume_eqs;
                 return true;
             }
         }
diff --git a/src/smt/theory_arith_pp.h b/src/smt/theory_arith_pp.h
index ee1268b79..8e9ef878e 100644
--- a/src/smt/theory_arith_pp.h
+++ b/src/smt/theory_arith_pp.h
@@ -35,6 +35,7 @@ namespace smt {
         st.update("arith assert diseq", m_stats.m_assert_diseq);
         st.update("arith bound prop", m_stats.m_bound_props);
         st.update("arith fixed eqs", m_stats.m_fixed_eqs);
+        st.update("arith assume eqs", m_stats.m_assume_eqs);
         st.update("arith offset eqs", m_stats.m_offset_eqs);
         st.update("arith gcd tests", m_stats.m_gcd_tests);
         st.update("arith ineq splits", m_stats.m_branches);
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index ccc78005d..f62f46ec7 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1583,13 +1583,13 @@ public:
               }
               tout << "\n"; );
         if (!m_use_nra_model && !m_nla) {
-            lp().random_update(vars.size(), vars.c_ptr());
+            // lp().random_update(vars.size(), vars.c_ptr());
         }
         m_model_eqs.reset();
         TRACE("arith", display(tout););
             
         unsigned old_sz = m_assume_eq_candidates.size();
-        bool result = false;
+        unsigned num_candidates = 0;
         int start = ctx().get_random_value();
         for (theory_var i = 0; i < sz; ++i) {
             theory_var v = (i + start) % sz;
@@ -1611,11 +1611,10 @@ public:
                       tout << mk_pp(n1->get_owner(), m) << " = " << mk_pp(n2->get_owner(), m) << "\n";
                       tout << "v" << v << " = " << "v" << other << "\n";);
                 m_assume_eq_candidates.push_back(std::make_pair(v, other));
-                result = true;
             }
         }
             
-        if (result) {
+        if (num_candidates > 0) {
             ctx().push_trail(restore_size_trail<context, std::pair<theory_var, theory_var>, false>(m_assume_eq_candidates, old_sz));
         }
 
@@ -1692,14 +1691,14 @@ public:
                 st = FC_GIVEUP;
                 break;
             }
-            if (assume_eqs()) {
-                ++m_stats.m_assume_eqs;
-                return FC_CONTINUE;
-            }    
             if (delayed_assume_eqs()) {
                 ++m_stats.m_assume_eqs;
                 return FC_CONTINUE;
             }
+            if (assume_eqs()) {
+                ++m_stats.m_assume_eqs;
+                return FC_CONTINUE;
+            }    
             if (m_not_handled != nullptr) {
                 TRACE("arith", tout << "unhandled operator " << mk_pp(m_not_handled, m) << "\n";);        
                 st = FC_GIVEUP;