#7027

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Dec 2, 2023 · 331507c · 331507c
1 parent 7eab26e
commit 331507c
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 7 deletions.
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
@@ -53,17 +53,22 @@ namespace arith {
 
     euf::th_solver* solver::clone(euf::solver& dst_ctx) {
         arith::solver* result = alloc(arith::solver, dst_ctx, get_id());
+        unsigned_vector var2var;
+        for (unsigned i = 0; i < result->get_num_vars(); ++i) 
+            var2var.push_back(i);
+
         for (unsigned i = result->get_num_vars(); i < get_num_vars(); ++i) 
-            result->mk_evar(ctx.copy(dst_ctx, var2enode(i))->get_expr());        
+            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) {            
+            auto w = var2var[v];
             for (auto* b : bounds) {
-                auto* b2 = result->mk_var_bound(b->get_lit(), v, b->get_bound_kind(), b->get_value());
-                result->m_bounds[v].push_back(b2);
-                result->m_bounds_trail.push_back(v);
-                result->updt_unassigned_bounds(v, +1);
+                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);
             }

diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp
@@ -425,7 +425,7 @@ namespace euf {
         // not marked as shared.
 
         for (auto const& p : euf::enode_th_vars(n)) 
-            if (fid2solver(p.get_id())->is_shared(p.get_var())) {
+            if (fid2solver(p.get_id()) && fid2solver(p.get_id())->is_shared(p.get_var())) {
                 n->set_is_shared(l_true);
                 return true;
             }
@@ -436,7 +436,7 @@ namespace euf {
 
     bool solver::is_beta_redex(enode* p, enode* n) const {
         for (auto const& th : enode_th_vars(p))
-            if (fid2solver(th.get_id())->is_beta_redex(p, n))
+            if (fid2solver(th.get_id()) && fid2solver(th.get_id())->is_beta_redex(p, n))
                 return true;
         return false;
     }