From 362d299a5ccfd6f4daad533d8209a1a28c9b0463 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 2 Dec 2023 19:34:36 -0800
Subject: [PATCH] #7027

---
 src/sat/smt/arith_solver.cpp | 9 ++++-----
 src/sat/smt/euf_solver.h     | 1 +
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 9cf41412a59..2be9b6b600c 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -60,11 +60,11 @@ namespace arith {
         for (unsigned i = result->get_num_vars(); i < get_num_vars(); ++i) 
             var2var.push_back(result->mk_evar(ctx.copy(dst_ctx, var2enode(i))->get_expr()));
 
-        unsigned v = 0;
-        result->m_bounds.resize(m_bounds.size());
-        for (auto const& bounds : m_bounds) {            
+        result->m_bounds.resize(get_num_vars());
+        unsigned nv = std::min(m_bounds.size(), get_num_vars());
+        for (unsigned v = 0; v < nv; ++v) {
             auto w = var2var[v];
-            for (auto* b : bounds) {
+            for (auto* b : m_bounds[v]) {
                 auto* b2 = result->mk_var_bound(b->get_lit(), w, b->get_bound_kind(), b->get_value());
                 result->m_bounds[w].push_back(b2);
                 result->m_bounds_trail.push_back(w);
@@ -72,7 +72,6 @@ namespace arith {
                 result->m_bool_var2bound.insert(b->get_lit().var(), b2);
                 result->m_new_bounds.push_back(b2);
             }
-            ++v;
         }
 
         // clone rows into m_solver, m_nla, m_lia
diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h
index a9dc20e0e6a..4121b68c9b9 100644
--- a/src/sat/smt/euf_solver.h
+++ b/src/sat/smt/euf_solver.h
@@ -348,6 +348,7 @@ namespace euf {
         bool is_external(bool_var v) override;
         bool propagated(literal l, ext_constraint_idx idx) override;
         bool unit_propagate() override;
+        bool should_propagate() override;
         bool should_research(sat::literal_vector const& core) override;
         void add_assumptions(sat::literal_set& assumptions) override;
         bool tracking_assumptions() override;