diff --git a/z3-data-race.patch b/z3-data-race.patch new file mode 100644 index 0000000..547b48c --- /dev/null +++ b/z3-data-race.patch @@ -0,0 +1,10 @@ +--- z3-z3-4.11.2/src/solver/parallel_tactic.cpp.orig 2022-09-03 16:47:12.000000000 -0600 ++++ z3-z3-4.11.2/src/solver/parallel_tactic.cpp 2023-01-08 21:39:29.169670155 -0700 +@@ -460,6 +460,7 @@ private: + conquer->get_model(mdl); + } + else { ++ std::lock_guard lock(m_mutex); + s.get_solver().get_model(mdl); + } + if (mdl) { diff --git a/z3-uninit.patch b/z3-uninit.patch new file mode 100644 index 0000000..fc3623c --- /dev/null +++ b/z3-uninit.patch @@ -0,0 +1,10 @@ +--- z3-z3-4.11.2/src/sat/sat_lookahead.cpp.orig 2022-09-03 16:47:12.000000000 -0600 ++++ z3-z3-4.11.2/src/sat/sat_lookahead.cpp 2023-01-06 15:09:19.198322817 -0700 +@@ -1001,6 +1001,7 @@ namespace sat { + m_inconsistent = false; + m_qhead = 0; + m_bstamp_id = 0; ++ m_istamp_id = 0; + + for (unsigned i = 0; i < m_num_vars; ++i) { + init_var(i); diff --git a/z3.spec b/z3.spec index 7286398..57ea922 100644 --- a/z3.spec +++ b/z3.spec @@ -7,7 +7,7 @@ Name: z3 Version: 4.8.17 -Release: 1%{?dist} +Release: 2%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -15,6 +15,10 @@ URL: https://github.com/Z3Prover/z3 Source0: https://github.com/Z3Prover/z3/archive/%{name}-%{version}.tar.gz # Change the way python finds the shared object; see bz 1910923 Patch0: %{name}-python.patch + # Fix use of an uninitialized variable +Patch1: %{name}-uninit.patch +# Fix a data race that can cause a segfault; see bz 2157972 +Patch2: %{name}-data-race.patch BuildRequires: cmake BuildRequires: doxygen @@ -232,6 +236,10 @@ cd - %{python3_sitelib}/%{name}/ %changelog +* Mon Jan 9 2023 Jerry James - 4.8.17-2 +- Add -data-race patch to fix segfault (bz 2157972) +- Add -uninit patch to fix use of an uninitialized value + * Mon May 16 2022 Jerry James - 4.8.17-1 - Version 4.8.17 - Drop upstreamed -ambiguous-overload patch