Unverified Commit d15b6fd3 authored by Florian Brandes's avatar Florian Brandes
Browse files

z3: fix memory corruption 



fixes #486491

Signed-off-by: default avatarFlorian Brandes <florian.brandes@posteo.de>
parent 795254bb

pkgs/by-name/z3/z3/package.nix

+20 −0
Original line number Diff line number Diff line
@@ -2,6 +2,7 @@ 
  lib,

  stdenv,

  fetchFromGitHub,

  fetchpatch2,

  python3Packages,

  fixDarwinDylibNames,

  nix-update-script,
@@ -39,6 +40,25 @@ stdenv.mkDerivation (finalAttrs: { 


  patches = lib.optionals useCmakeBuild [

    ./fix-pkg-config-paths.patch

    # fix Segmentation fault. See https://github.com/Z3Prover/z3/pull/8264 and

    # https://github.com/NixOS/nixpkgs/issues/486491

    (fetchpatch2 {

      name = "preserve-the-initial-state-of-the-solver.patch";

      url = "https://github.com/Z3Prover/z3/commit/850a3236adab92f9f6f569ac66ffbb69be179f4c.patch?full_index=1";

      hash = "sha256-C6p+dj3i3DpOnd2wr+R8ZwClHoMFfk5i5/+JRhTDNcs=";

    })

    # needs to include a cosmetic change to apply patch for memory corruption

    (fetchpatch2 {

      name = "cosmetic-changes-to-i.patch";

      url = "https://github.com/Z3Prover/z3/commit/243694379475d983605f87578452a330f3e3b28f.patch?full_index=1";

      includes = [ "src/api/api_polynomial.cpp" ];

      hash = "sha256-huo5S73WrFrEEUcaP+1LDQwGwo+n2iYT4x/OjK5rmqQ=";

    })

    (fetchpatch2 {

      name = "fix-memory-corruption.patch";

      url = "https://github.com/Z3Prover/z3/commit/e7b6f3f33bcc6c88a0f2ace47ff2f09b59239433.patch?full_index=1";

      hash = "sha256-kEEeod4s8i9SI2e2TFD2U4yd1qEPoGnJOfE0y+1Cq6M=";

    })

  ];



  strictDeps = true;