add cvc5 to Nix config, fix all timeouts

Author: nmouha

flake.nix

@@ -25,7 +25,7 @@
           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) bitwuzla cvc5 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;
@@ -237,7 +237,7 @@
             pkgs-unstable = inputs.nixpkgs-unstable.legacyPackages.x86_64-linux;
             util = pkgs.callPackage ./nix/util.nix {
               inherit pkgs;
-              inherit (pkgs) bitwuzla z3;
+              inherit (pkgs) bitwuzla cvc5 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;

nix/cbmc/default.nix

@@ -3,6 +3,7 @@
 # SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
 { buildEnv
 , cbmc
+, cvc5
 , fetchFromGitHub
 , callPackage
 , bitwuzla
@@ -37,6 +38,7 @@ buildEnv {
 
       inherit
         bitwuzla# 0.8.2
+        cvc5# 1.3.2
         ninja; # 1.13.2
     };
 }

nix/util.nix

@@ -2,7 +2,7 @@
 # Copyright (c) The mldsa-native project authors
 # SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
 
-{ pkgs, cbmc, bitwuzla, z3, python3-for-slothy }:
+{ pkgs, cbmc, bitwuzla, cvc5, z3, python3-for-slothy }:
 rec {
   glibc-join = p: p.buildPackages.symlinkJoin {
     name = "glibc-join";
@@ -96,7 +96,7 @@ rec {
     };
   };
 
-  cbmc_pkgs = pkgs.callPackage ./cbmc { inherit cbmc bitwuzla z3; };
+  cbmc_pkgs = pkgs.callPackage ./cbmc { inherit cbmc bitwuzla cvc5 z3; };
 
   valgrind_varlat = pkgs.callPackage ./valgrind { };
   hol_light' = pkgs.callPackage ./hol_light { };

proofs/cbmc/indcpa_dec/Makefile

@@ -37,7 +37,7 @@ USE_DYNAMIC_FRAMES=1
 
 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
 EXTERNAL_SAT_SOLVER=
-CBMCFLAGS=--smt2
+CBMCFLAGS=--cvc5 --refine-arrays
 
 FUNCTION_NAME = mlk_indcpa_dec
 

proofs/cbmc/indcpa_enc/Makefile

@@ -43,7 +43,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_smt_only --z3
+CBMCFLAGS=--cvc5 --refine-arrays
 
 FUNCTION_NAME = mlk_indcpa_enc
 

proofs/cbmc/indcpa_keypair_derand/Makefile

@@ -36,7 +36,7 @@ USE_DYNAMIC_FRAMES=1
 
 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
 EXTERNAL_SAT_SOLVER=
-CBMCFLAGS=--smt2
+CBMCFLAGS=--cvc5 --refine-arrays
 
 FUNCTION_NAME = mlk_indcpa_keypair_derand
 

proofs/cbmc/keccak_squeeze_once/Makefile

@@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1
 
 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
 EXTERNAL_SAT_SOLVER=
-CBMCFLAGS=--bitwuzla
+CBMCFLAGS=--z3
 
 FUNCTION_NAME = mlk_keccak_squeeze_once
 

proofs/cbmc/nttunpack_native_x86_64/Makefile

@@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1
 
 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
 EXTERNAL_SAT_SOLVER=
-CBMCFLAGS=--smt2
+CBMCFLAGS=--cvc5 --refine-arrays
 
 FUNCTION_NAME = nttunpack_native_x86_64
 

proofs/cbmc/poly_ntt_native/Makefile

@@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1
 
 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
 EXTERNAL_SAT_SOLVER=
-CBMCFLAGS=--bitwuzla
+CBMCFLAGS=--cvc5 --refine-arrays
 
 FUNCTION_NAME = mlk_poly_ntt
 

proofs/cbmc/poly_reduce_native/Makefile

@@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1
 
 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
 EXTERNAL_SAT_SOLVER=
-CBMCFLAGS=--bitwuzla
+CBMCFLAGS=--cvc5 --refine-arrays
 
 FUNCTION_NAME = mlk_poly_reduce_native