From c1944418245482883034ea9435b66a38cabeb4f7 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 4 Jun 2021 10:17:53 -0700
Subject: [PATCH] #5324

---
 src/sat/smt/arith_solver.cpp | 23 ++++++++++++++++-------
 src/sat/smt/euf_model.cpp    |  6 ++++--
 2 files changed, 20 insertions(+), 9 deletions(-)

diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 988e3070168..6b3dc752ace 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -138,26 +138,31 @@ namespace arith {
         lp_api::bound_kind k = b.get_bound_kind();
         theory_var v = b.get_var();
         inf_rational val = b.get_value(is_true);
+        bool same_polarity = b.get_lit().sign() == lit1.sign();
         lp_bounds const& bounds = m_bounds[v];
         SASSERT(!bounds.empty());
         if (bounds.size() == 1) return;
         if (m_unassigned_bounds[v] == 0) return;
         bool v_is_int = b.is_int();
         literal lit2 = sat::null_literal;
-        bool find_glb = (is_true == (k == lp_api::lower_t));
+        bool find_glb = (same_polarity == (k == lp_api::lower_t));
         TRACE("arith", tout << lit1 << " v" << v << " val " << val << " find_glb: " << find_glb << " is_true: " << is_true << " k: " << k << " is_lower: " << (k == lp_api::lower_t) << "\n";);
         if (find_glb) {
             rational glb;
             api_bound* lb = nullptr;
             for (api_bound* b2 : bounds) {
-                if (b2 == &b) continue;
+                if (b2 == &b) 
+                    continue;
                 rational const& val2 = b2->get_value();
-                if (((is_true || v_is_int) ? val2 < val : val2 <= val) && (!lb || glb < val2)) {
+                if (lb && glb >= val2)
+                    continue;
+                if (((same_polarity || v_is_int) ? val2 < val : val2 <= val)) {
                     lb = b2;
                     glb = val2;
                 }
             }
-            if (!lb) return;
+            if (!lb) 
+                return;
             bool sign = lb->get_bound_kind() != lp_api::lower_t;
             lit2 = lb->get_lit();
             if (sign)
@@ -167,14 +172,18 @@ namespace arith {
             rational lub;
             api_bound* ub = nullptr;
             for (api_bound* b2 : bounds) {
-                if (b2 == &b) continue;
+                if (b2 == &b) 
+                    continue;
                 rational const& val2 = b2->get_value();
-                if (((is_true || v_is_int) ? val < val2 : val <= val2) && (!ub || val2 < lub)) {
+                if (ub && val2 >= lub)
+                    continue;
+                if (((same_polarity || v_is_int) ? val < val2 : val <= val2)) {
                     ub = b2;
                     lub = val2;
                 }
             }
-            if (!ub) return;
+            if (!ub) 
+                return;
             bool sign = ub->get_bound_kind() != lp_api::upper_t;
             lit2 = ub->get_lit();
             if (sign)
diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp
index 3669fb52eed..886d37a58e9 100644
--- a/src/sat/smt/euf_model.cpp
+++ b/src/sat/smt/euf_model.cpp
@@ -209,8 +209,10 @@ namespace euf {
                     mdl->register_decl(f, fi);
                 }
                 args.reset();                
-                for (enode* arg : enode_args(n)) 
-                    args.push_back(m_values.get(arg->get_root_id()));                
+                for (expr* arg : *a) {
+                    enode* earg = get_enode(arg); 
+                    args.push_back(m_values.get(earg->get_root_id()));                
+                }
                 DEBUG_CODE(for (expr* arg : args) VERIFY(arg););
                 SASSERT(args.size() == arity);
                 if (!fi->get_entry(args.data()))