From 9cfbd623ec1ce44aac24c9cc4f645e9128404164 Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Fri, 22 May 2026 11:52:23 +0800 Subject: [PATCH 1/2] nix: Pin z3 to upstream commit 286b107 Signed-off-by: Matthias J. Kannwischer --- flake.lock | 6 +++--- flake.nix | 8 ++++---- nix/cbmc/default.nix | 6 +++--- 3 files changed, 10 insertions(+), 10 deletions(-) diff --git a/flake.lock b/flake.lock index a32a39acf..89e625881 100644 --- a/flake.lock +++ b/flake.lock @@ -54,11 +54,11 @@ }, "nixpkgs-unstable": { "locked": { - "lastModified": 1776877367, - "narHash": "sha256-EHq1/OX139R1RvBzOJ0aMRT3xnWyqtHBRUBuO1gFzjI=", + "lastModified": 1778869304, + "narHash": "sha256-30sZNZoA1cqF5JNO9fVX+wgiQYjB7HJqqJ4ztCDeBZE=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "0726a0ecb6d4e08f6adced58726b95db924cef57", + "rev": "d233902339c02a9c334e7e593de68855ad26c4cb", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index 7714eec95..028638ad3 100644 --- a/flake.nix +++ b/flake.nix @@ -25,8 +25,8 @@ pkgs-unstable = inputs.nixpkgs-unstable.legacyPackages.${system}; pkgs-2405 = inputs.nixpkgs-2405.legacyPackages.${system}; util = pkgs.callPackage ./nix/util.nix { - inherit (pkgs) bitwuzla z3; - inherit (pkgs-unstable) cbmc; + inherit (pkgs) bitwuzla; + inherit (pkgs-unstable) cbmc z3; # TODO: switch back to stable python3 for slothy once ortools is fixed in 25.11 python3-for-slothy = pkgs-unstable.python3; }; @@ -240,8 +240,8 @@ pkgs-unstable = inputs.nixpkgs-unstable.legacyPackages.x86_64-linux; util = pkgs.callPackage ./nix/util.nix { inherit pkgs; - inherit (pkgs) bitwuzla z3; - inherit (pkgs-unstable) cbmc; + inherit (pkgs) bitwuzla; + inherit (pkgs-unstable) cbmc z3; # TODO: switch back to stable python3 for slothy once ortools is fixed in 25.11 python3-for-slothy = pkgs-unstable.python3; }; diff --git a/nix/cbmc/default.nix b/nix/cbmc/default.nix index 58e21c796..bb0d89c32 100644 --- a/nix/cbmc/default.nix +++ b/nix/cbmc/default.nix @@ -26,12 +26,12 @@ buildEnv { litani = callPackage ./litani.nix { }; # 1.29.0 cbmc-viewer = callPackage ./cbmc-viewer.nix { }; # 3.12 z3 = z3.overrideAttrs (_: { - version = "4.15.3"; + version = "4.17.0"; src = fetchFromGitHub { owner = "Z3Prover"; repo = "z3"; - rev = "z3-4.15.3"; - hash = "sha256-Lw037Z0t0ySxkgMXkbjNW5CB4QQLRrrSEBsLJqiomZ4="; + rev = "286b107d7da5d357b76d318e8b23eb9aa219d143"; + hash = "sha256-Qjb/YK5TxU0WKF3RPJ/pUmxB2qqgPnY3OSRSkKM/s3c="; }; }); From 1da0e32399c27adb8fc6cbd094b5c7ac3d6ecfa7 Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Fri, 22 May 2026 21:16:41 +0800 Subject: [PATCH 2/2] CBMC: Switch polyvec_matrix_pointwise_montgomery_row to z3_smt_only Signed-off-by: Matthias J. Kannwischer --- proofs/cbmc/polyvec_matrix_pointwise_montgomery_row/Makefile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/proofs/cbmc/polyvec_matrix_pointwise_montgomery_row/Makefile b/proofs/cbmc/polyvec_matrix_pointwise_montgomery_row/Makefile index 122b3f8a7..dec81bd1e 100644 --- a/proofs/cbmc/polyvec_matrix_pointwise_montgomery_row/Makefile +++ b/proofs/cbmc/polyvec_matrix_pointwise_montgomery_row/Makefile @@ -33,7 +33,7 @@ USE_DYNAMIC_FRAMES=1 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--external-smt2-solver $(PROOF_ROOT)/lib/z3_no_bv_extract --z3 +CBMCFLAGS=--external-smt2-solver $(PROOF_ROOT)/lib/z3_smt_only --z3 FUNCTION_NAME = polyvec_matrix_pointwise_montgomery_row @@ -44,7 +44,7 @@ FUNCTION_NAME = polyvec_matrix_pointwise_montgomery_row EXPENSIVE = true # This function is large enough to need... -CBMC_OBJECT_BITS = 11 +CBMC_OBJECT_BITS = 8 # If you require access to a file-local ("static") function or object to conduct # your proof, set the following (and do not include the original source file