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 1803e4a..9328599 100644 --- a/z3.spec +++ b/z3.spec @@ -16,7 +16,7 @@ Name: z3 Version: 4.11.2 -Release: 1%{?dist} +Release: 2%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -24,6 +24,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 @@ -168,8 +172,8 @@ sed -e '/libz3java/s,\(System\.load\)Library("\(.*\)"),\1("%{_libdir}/z3/\2.so") -i scripts/update_api.py %build -export LANG="C.UTF-8" -export PYTHON="%{python3}" +export LANG=C.UTF-8 +export PYTHON=%{python3} %cmake -G Ninja \ -DCMAKE_INSTALL_INCLUDEDIR=%{_includedir}/z3 \ @@ -284,6 +288,10 @@ cd - %{python3_sitelib}/z3/ %changelog +* Sun Jan 8 2023 Jerry James - 4.11.2-2 +- Add -data-race patch to fix segfault (bz 2157972) +- Add -uninit patch to fix use of an uninitialized value + * Wed Dec 14 2022 Jerry James - 4.11.2-1 - Further clarify license of the doc subpackage (SPDX)