nix: Pull CBMC 6.9.0 from nixos-unstable binary cache

CBMC 6.9.0 is now available in nixos-unstable, so we can fetch it
prebuilt instead of rebuilding from source.

Also drop the standalone cadical binary from the CBMC package env,
the CI version-summary line, and print_tool_versions.py: cbmc
bundles its own cadical internally, so the standalone one on PATH
did not reflect the solver actually used.

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

Author: mkannwischer

.github/actions/cbmc/action.yml

@@ -46,7 +46,6 @@ runs:
               - $(nix --version)
               - $(cbmc --version)
               - litani Version $(litani --version)
-              - Cadical Version $(cadical --version)
               - $(bash --version | grep -m1 "")
             EOF
       - name: Run CBMC proofs (MLKEM_K=${{ inputs.mlkem_k }})

flake.lock

@@ -25,7 +25,8 @@
           pkgs-unstable = inputs.nixpkgs-unstable.legacyPackages.${system};
           pkgs-2405 = inputs.nixpkgs-2405.legacyPackages.${system};
           util = pkgs.callPackage ./nix/util.nix {
-            inherit (pkgs) cbmc bitwuzla z3;
+            inherit (pkgs) bitwuzla z3;
+            inherit (pkgs-unstable) cbmc;
             # TODO: switch back to stable python3 for slothy once ortools is fixed in 25.11
             python3-for-slothy = pkgs-unstable.python3;
           };
@@ -223,7 +224,8 @@
             pkgs-unstable = inputs.nixpkgs-unstable.legacyPackages.x86_64-linux;
             util = pkgs.callPackage ./nix/util.nix {
               inherit pkgs;
-              inherit (pkgs) cbmc bitwuzla z3;
+              inherit (pkgs) bitwuzla z3;
+              inherit (pkgs-unstable) cbmc;
               # TODO: switch back to stable python3 for slothy once ortools is fixed in 25.11
               python3-for-slothy = pkgs-unstable.python3;
             };

flake.nix

@@ -7,37 +7,25 @@
 , callPackage
 , bitwuzla
 , ninja
-, cadical
 , z3
-, cudd
-, replaceVars
-, fetchpatch
 }:
 
 buildEnv {
   name = "pqcp-cbmc";
   paths =
     builtins.attrValues {
-      cbmc = cbmc.overrideAttrs (old: rec {
+      cbmc = cbmc.overrideAttrs (_: {
         version = "6.9.0";
         src = fetchFromGitHub {
           owner = "diffblue";
           repo = "cbmc";
           hash = "sha256-SMJBnzoyTwcwJa9L2X1iX2W4Z/Mwoirf8EXfoyG0dRI=";
           tag = "cbmc-6.9.0";
         };
-        srccadical = cadical.src;
-        patches = [
-          (builtins.elemAt old.patches 0) # cudd patch from nixpkgs
-          ./0002-Do-not-download-sources-in-cmake.patch
-        ];
-        env = old.env // {
-          NIX_CFLAGS_COMPILE = (old.env.NIX_CFLAGS_COMPILE or "") + " -Wno-error=switch-enum";
-        };
       });
       litani = callPackage ./litani.nix { }; # 1.29.0
       cbmc-viewer = callPackage ./cbmc-viewer.nix { }; # 3.12
-      z3 = z3.overrideAttrs (old: rec {
+      z3 = z3.overrideAttrs (_: {
         version = "4.15.3";
         src = fetchFromGitHub {
           owner = "Z3Prover";
@@ -48,7 +36,6 @@ buildEnv {
       });
 
       inherit
-        cadical# 3.0.0
         bitwuzla# 0.8.2
         ninja; # 1.13.2
     };

nix/cbmc/0002-Do-not-download-sources-in-cmake.patch

@@ -11,7 +11,6 @@
 
 
 _TOOLS = [
-    "cadical",
     "cbmc",
     "cbmc-viewer",
     "litani",