From e1661759db682beaac8f3292bb23282071f6091c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 10 Jun 2025 15:55:54 -0700
Subject: [PATCH] update version to 4.15.2

---
 CMakeLists.txt                                |  2 +-
 MODULE.bazel                                  |  2 +-
 scripts/mk_project.py                         |  2 +-
 scripts/nightly.yaml                          |  2 +-
 scripts/release.yml                           |  2 +-
 .../portfolio/euf_completion_tactic.cpp       | 28 +++++++++++++++----
 6 files changed, 27 insertions(+), 11 deletions(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 372218006..f4c824670 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -2,7 +2,7 @@
 cmake_minimum_required(VERSION 3.16)
 
 set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake")
-project(Z3 VERSION 4.15.1.0 LANGUAGES CXX)
+project(Z3 VERSION 4.15.2.0 LANGUAGES CXX)
 
 ################################################################################
 # Project version
diff --git a/MODULE.bazel b/MODULE.bazel
index 60f5ad456..4548c7850 100644
--- a/MODULE.bazel
+++ b/MODULE.bazel
@@ -1,6 +1,6 @@
 module(
     name = "z3",
-    version = "4.14.0",
+    version = "4.15.2",
     bazel_compatibility = [">=7.0.0"],
 )
 
diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index 6b5197fa5..c78a2ce48 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -8,7 +8,7 @@
 from mk_util import *
 
 def init_version():
-    set_version(4, 15, 1, 0) # express a default build version or pick up ci build version
+    set_version(4, 15, 2, 0) # express a default build version or pick up ci build version
     
 # Z3 Project definition
 def init_project_def():
diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml
index db62beed2..a998179da 100644
--- a/scripts/nightly.yaml
+++ b/scripts/nightly.yaml
@@ -1,7 +1,7 @@
 variables:
   Major: '4'
   Minor: '15'
-  Patch: '1'
+  Patch: '2'
   ReleaseVersion: $(Major).$(Minor).$(Patch)
   AssemblyVersion: $(Major).$(Minor).$(Patch).$(Build.BuildId)
   NightlyVersion: $(AssemblyVersion)-$(Build.buildId)
diff --git a/scripts/release.yml b/scripts/release.yml
index e5a334131..258a54fb1 100644
--- a/scripts/release.yml
+++ b/scripts/release.yml
@@ -6,7 +6,7 @@
 trigger: none
 
 variables:
-  ReleaseVersion: '4.15.1'
+  ReleaseVersion: '4.15.2'
 
 stages:
 
diff --git a/src/tactic/portfolio/euf_completion_tactic.cpp b/src/tactic/portfolio/euf_completion_tactic.cpp
index 8fda726ac..a418c43c6 100644
--- a/src/tactic/portfolio/euf_completion_tactic.cpp
+++ b/src/tactic/portfolio/euf_completion_tactic.cpp
@@ -15,6 +15,7 @@ Author:
 
 --*/
 
+#include "ast/rewriter/expr_safe_replace.h"
 #include "tactic/tactic.h"
 #include "tactic/portfolio/euf_completion_tactic.h"
 #include "solver/solver.h"
@@ -25,7 +26,7 @@ class euf_side_condition_solver : public euf::side_condition_solver {
     params_ref m_params;
     scoped_ptr<solver> m_solver;
     expr_ref_vector m_deps;
-    obj_map<expr, expr_dependency*> m_e2d;
+    obj_map<expr, std::pair<proof*, expr_dependency*>> m_e2d;
     expr_ref_vector m_fmls;
     obj_hashtable<expr> m_seen;
     trail_stack m_trail;
@@ -55,7 +56,7 @@ public:
         m_solver->pop(n);
     }
 
-    void add_constraint(expr* f, expr_dependency* d) override {
+    void add_constraint(expr* f, proof* pr, expr_dependency* d) override {
         if (m_seen.contains(f))
             return;
         m_seen.insert(f);
@@ -68,7 +69,7 @@ public:
         if (d) {
             expr* e_dep = m.mk_fresh_const("dep", m.mk_bool_sort());
             m_deps.push_back(e_dep);
-            m_e2d.insert(e_dep, d);
+            m_e2d.insert(e_dep, { pr, d });
             m_trail.push(insert_obj_map(m_e2d, e_dep));
             m_solver->assert_expr(f, e_dep);
         }
@@ -76,7 +77,7 @@ public:
             m_solver->assert_expr(f);        
     }
 
-    bool is_true(expr* f, expr_dependency*& d) override {
+    bool is_true(expr* f, proof_ref& pr, expr_dependency*& d) override {
         d = nullptr;
         solver::scoped_push _sp(*m_solver);
         m_fmls.reset();
@@ -86,9 +87,24 @@ public:
         if (r == l_false) {
             expr_ref_vector core(m);
             m_solver->get_unsat_core(core);
-            for (auto c : core)
-                d = m.mk_join(d, m_e2d[c]);
+            for (auto c : core) {
+                auto [pr, dep] = m_e2d[c];
+                d = m.mk_join(d, dep);
+            }
+            if (m.proofs_enabled()) {
+                pr = m_solver->get_proof();
+                SASSERT(pr);
+                expr_safe_replace rep(m);
+                for (auto c : core) {
+                    auto [p, dep] = m_e2d[c];
+                    rep.insert(m.mk_asserted(c), p);
+                }
+                expr_ref ppr(pr, m);
+                rep(ppr);
+                pr = to_app(ppr.get());
+            }
         }
+
         return r == l_false;
     }