update version to 4.15.2

Author: NikolajBjorner

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

MODULE.bazel

@@ -1,6 +1,6 @@
 module(
     name = "z3",
-    version = "4.14.0",
+    version = "4.15.2",
     bazel_compatibility = [">=7.0.0"],
 )
 

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():

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)

scripts/release.yml

@@ -6,7 +6,7 @@
 trigger: none
 
 variables:
-  ReleaseVersion: '4.15.1'
+  ReleaseVersion: '4.15.2'
 
 stages:
 

src/tactic/portfolio/euf_completion_tactic.cpp

@@ -15,6 +15,7 @@ Module Name:
 
 --*/
 
+#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 @@ class euf_side_condition_solver : public euf::side_condition_solver {
         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,15 +69,15 @@ class euf_side_condition_solver : public euf::side_condition_solver {
         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);
         }
         else
             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 @@ class euf_side_condition_solver : public euf::side_condition_solver {
         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;
     }