#7027

src/sat/smt/arith_solver.cpp

@@ -60,19 +60,18 @@ 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);
                 result->updt_unassigned_bounds(w, +1);
                 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

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;