From 15fe7d653b549feb4e5cc5bbb867f998af34e132 Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Wed, 9 Sep 2026 22:53:33 +0800 Subject: [PATCH] CBMC: Use a second solver for 149/215 proofs A soundness bug in a single SMT solver would silently invalidate every proof discharged by it. To mitigate this risk, we aim to have each proof discharged by at least two solvers. 149 of 215 proofs gain a second solver: 98 bitwuzla, 25 cvc5_arrays_exp, and 26 Z3 profiles alongside a bitwuzla or cvc5 default. The other 66 do not, mostly because bitwuzla timed out or cvc5 returned unknown, either under a local 300s per-proof cap or in CI. Signed-off-by: Matthias J. Kannwischer --- proofs/cbmc/H/Makefile | 4 +++- proofs/cbmc/caddq/Makefile | 4 +++- proofs/cbmc/check_pct/Makefile | 4 +++- proofs/cbmc/ct_cmask_neg_i32/Makefile | 4 +++- proofs/cbmc/ct_cmask_nonzero_u32/Makefile | 4 +++- proofs/cbmc/ct_cmask_nonzero_u8/Makefile | 4 +++- proofs/cbmc/ct_get_optblocker_i64/Makefile | 4 +++- proofs/cbmc/ct_get_optblocker_u32/Makefile | 4 +++- proofs/cbmc/ct_get_optblocker_u8/Makefile | 4 +++- proofs/cbmc/ct_memcmp/Makefile | 4 +++- proofs/cbmc/ct_sel_int32/Makefile | 4 +++- proofs/cbmc/decompose/Makefile | 4 +++- proofs/cbmc/fqmul/Makefile | 4 +++- proofs/cbmc/fqscale/Makefile | 4 +++- proofs/cbmc/intt_native_aarch64/Makefile | 4 +++- proofs/cbmc/intt_native_x86_64/Makefile | 4 +++- proofs/cbmc/keccak_absorb/Makefile | 4 +++- proofs/cbmc/keccak_absorb_once_x4/Makefile | 4 +++- proofs/cbmc/keccak_f1600_x1_native_aarch64/Makefile | 4 +++- proofs/cbmc/keccak_f1600_x1_native_aarch64_v84a/Makefile | 4 +++- proofs/cbmc/keccak_f1600_x4_native_aarch64_v84a/Makefile | 4 +++- .../keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid/Makefile | 4 +++- .../Makefile | 4 +++- proofs/cbmc/keccak_f1600_x4_native_avx2/Makefile | 4 +++- proofs/cbmc/keccak_finalize/Makefile | 4 +++- proofs/cbmc/keccak_init/Makefile | 4 +++- proofs/cbmc/keccak_squeeze/Makefile | 4 +++- proofs/cbmc/keccak_squeezeblocks_x4/Makefile | 4 +++- proofs/cbmc/keccakf1600_extract_bytes/Makefile | 4 +++- proofs/cbmc/keccakf1600_extract_bytes_BE/Makefile | 4 +++- proofs/cbmc/keccakf1600_permute/Makefile | 4 +++- proofs/cbmc/keccakf1600_permute_c/Makefile | 4 +++- proofs/cbmc/keccakf1600_permute_native/Makefile | 4 +++- proofs/cbmc/keccakf1600_xor_bytes/Makefile | 4 +++- proofs/cbmc/keccakf1600_xor_bytes_BE/Makefile | 4 +++- proofs/cbmc/keccakf1600x4_extract_bytes/Makefile | 4 +++- proofs/cbmc/keccakf1600x4_extract_bytes_c/Makefile | 4 +++- proofs/cbmc/keccakf1600x4_extract_bytes_native/Makefile | 4 +++- proofs/cbmc/keccakf1600x4_permute/Makefile | 4 +++- proofs/cbmc/keccakf1600x4_permute_native/Makefile | 4 +++- proofs/cbmc/keccakf1600x4_xor_bytes/Makefile | 4 +++- proofs/cbmc/keccakf1600x4_xor_bytes_c/Makefile | 4 +++- proofs/cbmc/keccakf1600x4_xor_bytes_native/Makefile | 4 +++- proofs/cbmc/make_hint/Makefile | 4 +++- proofs/cbmc/montgomery_reduce/Makefile | 4 +++- proofs/cbmc/ntt_layer/Makefile | 4 +++- proofs/cbmc/ntt_native_aarch64/Makefile | 4 +++- proofs/cbmc/ntt_native_x86_64/Makefile | 4 +++- proofs/cbmc/pack_sig_c/Makefile | 4 +++- proofs/cbmc/pack_sig_h/Makefile | 4 +++- proofs/cbmc/pack_sig_z/Makefile | 4 +++- proofs/cbmc/pack_sk_rho_key_tr/Makefile | 4 +++- proofs/cbmc/pointwise_native_aarch64/Makefile | 4 +++- proofs/cbmc/pointwise_native_x86_64/Makefile | 4 +++- proofs/cbmc/poly_caddq/Makefile | 4 +++- proofs/cbmc/poly_caddq_c/Makefile | 4 +++- proofs/cbmc/poly_caddq_native/Makefile | 4 +++- proofs/cbmc/poly_caddq_native_x86_64/Makefile | 4 +++- proofs/cbmc/poly_challenge/Makefile | 4 +++- proofs/cbmc/poly_chknorm/Makefile | 4 +++- proofs/cbmc/poly_chknorm_c/Makefile | 4 +++- proofs/cbmc/poly_chknorm_native/Makefile | 4 +++- proofs/cbmc/poly_chknorm_native_aarch64/Makefile | 4 +++- proofs/cbmc/poly_chknorm_native_x86_64/Makefile | 4 +++- proofs/cbmc/poly_decompose/Makefile | 4 +++- proofs/cbmc/poly_decompose_88_native_aarch64/Makefile | 4 +++- proofs/cbmc/poly_invntt_tomont/Makefile | 4 +++- proofs/cbmc/poly_invntt_tomont_native/Makefile | 4 +++- proofs/cbmc/poly_ntt/Makefile | 4 +++- proofs/cbmc/poly_ntt_c/Makefile | 4 +++- proofs/cbmc/poly_ntt_native/Makefile | 4 +++- proofs/cbmc/poly_permute_bitrev_to_custom_optional/Makefile | 4 +++- .../poly_permute_bitrev_to_custom_optional_native/Makefile | 4 +++- proofs/cbmc/poly_pointwise_montgomery/Makefile | 4 +++- proofs/cbmc/poly_reduce/Makefile | 4 +++- proofs/cbmc/poly_shiftl/Makefile | 4 +++- proofs/cbmc/poly_sub/Makefile | 4 +++- proofs/cbmc/poly_use_hint_native_aarch64/Makefile | 4 +++- proofs/cbmc/poly_use_hint_native_x86_64/Makefile | 4 +++- proofs/cbmc/polyeta_pack/Makefile | 4 +++- proofs/cbmc/polyeta_unpack/Makefile | 4 +++- proofs/cbmc/polymat_expand_entry/Makefile | 4 +++- proofs/cbmc/polyt0_pack/Makefile | 4 +++- proofs/cbmc/polyt0_unpack/Makefile | 4 +++- proofs/cbmc/polyt1_pack/Makefile | 4 +++- proofs/cbmc/polyt1_unpack/Makefile | 4 +++- proofs/cbmc/polyw1_pack/Makefile | 4 +++- proofs/cbmc/polyw1_pack_32/Makefile | 4 +++- proofs/cbmc/polyw1_pack_88/Makefile | 4 +++- proofs/cbmc/polyw1_unpack/Makefile | 4 +++- proofs/cbmc/polyw1_unpack_32/Makefile | 4 +++- proofs/cbmc/polyw1_unpack_88/Makefile | 4 +++- proofs/cbmc/polyz_pack/Makefile | 4 +++- proofs/cbmc/polyz_unpack/Makefile | 4 +++- proofs/cbmc/polyz_unpack_17_native_aarch64/Makefile | 4 +++- proofs/cbmc/polyz_unpack_19_native_aarch64/Makefile | 4 +++- proofs/cbmc/polyz_unpack_c/Makefile | 4 +++- proofs/cbmc/polyz_unpack_native/Makefile | 4 +++- proofs/cbmc/polyz_unpack_native_x86_64/Makefile | 4 +++- proofs/cbmc/power2round/Makefile | 4 +++- proofs/cbmc/prepare_domain_separation_prefix/Makefile | 4 +++- proofs/cbmc/reduce32/Makefile | 4 +++- proofs/cbmc/rej_eta/Makefile | 4 +++- proofs/cbmc/rej_eta_c/Makefile | 4 +++- proofs/cbmc/rej_eta_native/Makefile | 4 +++- proofs/cbmc/rej_uniform/Makefile | 4 +++- proofs/cbmc/rej_uniform_c/Makefile | 4 +++- proofs/cbmc/rej_uniform_eta_native_aarch64/Makefile | 4 +++- proofs/cbmc/rej_uniform_eta_native_x86_64/Makefile | 4 +++- proofs/cbmc/rej_uniform_native/Makefile | 4 +++- proofs/cbmc/rej_uniform_native_aarch64/Makefile | 4 +++- proofs/cbmc/rej_uniform_native_x86_64/Makefile | 4 +++- proofs/cbmc/shake128_absorb/Makefile | 4 +++- proofs/cbmc/shake128_finalize/Makefile | 4 +++- proofs/cbmc/shake128_init/Makefile | 4 +++- proofs/cbmc/shake128_release/Makefile | 4 +++- proofs/cbmc/shake128_squeeze/Makefile | 4 +++- proofs/cbmc/shake128x4_absorb_once/Makefile | 4 +++- proofs/cbmc/shake128x4_squeezeblocks/Makefile | 4 +++- proofs/cbmc/shake256/Makefile | 4 +++- proofs/cbmc/shake256_absorb/Makefile | 4 +++- proofs/cbmc/shake256_finalize/Makefile | 4 +++- proofs/cbmc/shake256_init/Makefile | 4 +++- proofs/cbmc/shake256_release/Makefile | 4 +++- proofs/cbmc/shake256_squeeze/Makefile | 4 +++- proofs/cbmc/shake256x4_absorb_once/Makefile | 4 +++- proofs/cbmc/shake256x4_squeezeblocks/Makefile | 4 +++- proofs/cbmc/sig_unpack_hints/Makefile | 4 +++- proofs/cbmc/sign_attempt/Makefile | 4 +++- proofs/cbmc/sign_finish/Makefile | 4 +++- proofs/cbmc/sign_resume/Makefile | 4 +++- proofs/cbmc/sign_signature/Makefile | 4 +++- proofs/cbmc/sign_signature_pre_hash_internal/Makefile | 4 +++- proofs/cbmc/sign_signature_pre_hash_shake256/Makefile | 4 +++- proofs/cbmc/sign_verify/Makefile | 4 +++- proofs/cbmc/sign_verify_extmu/Makefile | 4 +++- proofs/cbmc/sign_verify_pre_hash_internal/Makefile | 4 +++- proofs/cbmc/sign_verify_pre_hash_shake256/Makefile | 4 +++- proofs/cbmc/sk_s1hat_get_poly/Makefile | 4 +++- proofs/cbmc/sk_s2hat_get_poly/Makefile | 4 +++- proofs/cbmc/sk_t0hat_get_poly/Makefile | 4 +++- proofs/cbmc/sys_check_capability/Makefile | 4 +++- proofs/cbmc/unpack_pk_t1/Makefile | 4 +++- proofs/cbmc/use_hint/Makefile | 4 +++- proofs/cbmc/value_barrier_i64/Makefile | 4 +++- proofs/cbmc/value_barrier_u32/Makefile | 4 +++- proofs/cbmc/value_barrier_u8/Makefile | 4 +++- proofs/cbmc/yvec_get_poly/Makefile | 4 +++- proofs/cbmc/yvec_init/Makefile | 4 +++- 149 files changed, 447 insertions(+), 149 deletions(-) diff --git a/proofs/cbmc/H/Makefile b/proofs/cbmc/H/Makefile index 4ab52ec090..793d10bb37 100644 --- a/proofs/cbmc/H/Makefile +++ b/proofs/cbmc/H/Makefile @@ -30,7 +30,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = mld_h diff --git a/proofs/cbmc/caddq/Makefile b/proofs/cbmc/caddq/Makefile index 06f3746d72..a90438fd44 100644 --- a/proofs/cbmc/caddq/Makefile +++ b/proofs/cbmc/caddq/Makefile @@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = caddq diff --git a/proofs/cbmc/check_pct/Makefile b/proofs/cbmc/check_pct/Makefile index fb27325738..380b1b5fb9 100644 --- a/proofs/cbmc/check_pct/Makefile +++ b/proofs/cbmc/check_pct/Makefile @@ -28,7 +28,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = mld_check_pct diff --git a/proofs/cbmc/ct_cmask_neg_i32/Makefile b/proofs/cbmc/ct_cmask_neg_i32/Makefile index ca32a72fec..73c536aede 100644 --- a/proofs/cbmc/ct_cmask_neg_i32/Makefile +++ b/proofs/cbmc/ct_cmask_neg_i32/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:cvc5_arrays_exp CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = mld_ct_cmask_neg_i32 diff --git a/proofs/cbmc/ct_cmask_nonzero_u32/Makefile b/proofs/cbmc/ct_cmask_nonzero_u32/Makefile index 7e47ad46d6..db1d309d22 100644 --- a/proofs/cbmc/ct_cmask_nonzero_u32/Makefile +++ b/proofs/cbmc/ct_cmask_nonzero_u32/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:cvc5_arrays_exp CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = mld_ct_cmask_nonzero_u32 diff --git a/proofs/cbmc/ct_cmask_nonzero_u8/Makefile b/proofs/cbmc/ct_cmask_nonzero_u8/Makefile index 0aa354d5d3..59e2187216 100644 --- a/proofs/cbmc/ct_cmask_nonzero_u8/Makefile +++ b/proofs/cbmc/ct_cmask_nonzero_u8/Makefile @@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = mld_ct_cmask_nonzero_u8 diff --git a/proofs/cbmc/ct_get_optblocker_i64/Makefile b/proofs/cbmc/ct_get_optblocker_i64/Makefile index 77ca2d50d5..c2a0fccd8c 100644 --- a/proofs/cbmc/ct_get_optblocker_i64/Makefile +++ b/proofs/cbmc/ct_get_optblocker_i64/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = mld_ct_get_optblocker_i64 diff --git a/proofs/cbmc/ct_get_optblocker_u32/Makefile b/proofs/cbmc/ct_get_optblocker_u32/Makefile index 1c6c2d8563..9087d6fc49 100644 --- a/proofs/cbmc/ct_get_optblocker_u32/Makefile +++ b/proofs/cbmc/ct_get_optblocker_u32/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = mld_ct_get_optblocker_u32 diff --git a/proofs/cbmc/ct_get_optblocker_u8/Makefile b/proofs/cbmc/ct_get_optblocker_u8/Makefile index 0c7494048d..e446bc75d3 100644 --- a/proofs/cbmc/ct_get_optblocker_u8/Makefile +++ b/proofs/cbmc/ct_get_optblocker_u8/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:bitwuzla +CBMC_SUPPORTED_CONFIGS = \ + LP64:bitwuzla \ + LP64:z3_smt_only CBMC_DEFAULT_CONFIG = LP64:bitwuzla FUNCTION_NAME = mld_ct_get_optblocker_u8 diff --git a/proofs/cbmc/ct_memcmp/Makefile b/proofs/cbmc/ct_memcmp/Makefile index d9e089240c..099bce004b 100644 --- a/proofs/cbmc/ct_memcmp/Makefile +++ b/proofs/cbmc/ct_memcmp/Makefile @@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:bitwuzla +CBMC_SUPPORTED_CONFIGS = \ + LP64:bitwuzla \ + LP64:z3_no_bv_extract CBMC_DEFAULT_CONFIG = LP64:bitwuzla FUNCTION_NAME = mld_ct_memcmp diff --git a/proofs/cbmc/ct_sel_int32/Makefile b/proofs/cbmc/ct_sel_int32/Makefile index 3ebca3a525..52dd8d5355 100644 --- a/proofs/cbmc/ct_sel_int32/Makefile +++ b/proofs/cbmc/ct_sel_int32/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = mld_ct_sel_int32 diff --git a/proofs/cbmc/decompose/Makefile b/proofs/cbmc/decompose/Makefile index 53fca7d3cf..e9b106ebad 100644 --- a/proofs/cbmc/decompose/Makefile +++ b/proofs/cbmc/decompose/Makefile @@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = decompose diff --git a/proofs/cbmc/fqmul/Makefile b/proofs/cbmc/fqmul/Makefile index 67c4441f57..5e25bdd104 100644 --- a/proofs/cbmc/fqmul/Makefile +++ b/proofs/cbmc/fqmul/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:bitwuzla +CBMC_SUPPORTED_CONFIGS = \ + LP64:bitwuzla \ + LP64:z3_smt_only CBMC_DEFAULT_CONFIG = LP64:bitwuzla FUNCTION_NAME = mld_fqmul diff --git a/proofs/cbmc/fqscale/Makefile b/proofs/cbmc/fqscale/Makefile index 9f9fabb185..3c313c5063 100644 --- a/proofs/cbmc/fqscale/Makefile +++ b/proofs/cbmc/fqscale/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:bitwuzla +CBMC_SUPPORTED_CONFIGS = \ + LP64:bitwuzla \ + LP64:z3 CBMC_DEFAULT_CONFIG = LP64:bitwuzla FUNCTION_NAME = mld_fqscale diff --git a/proofs/cbmc/intt_native_aarch64/Makefile b/proofs/cbmc/intt_native_aarch64/Makefile index 2ee074b2d1..f86b4276d8 100644 --- a/proofs/cbmc/intt_native_aarch64/Makefile +++ b/proofs/cbmc/intt_native_aarch64/Makefile @@ -28,7 +28,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = intt_native_aarch64 diff --git a/proofs/cbmc/intt_native_x86_64/Makefile b/proofs/cbmc/intt_native_x86_64/Makefile index 375ea81ff2..9114ffcbce 100644 --- a/proofs/cbmc/intt_native_x86_64/Makefile +++ b/proofs/cbmc/intt_native_x86_64/Makefile @@ -28,7 +28,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = intt_native_x86_64 diff --git a/proofs/cbmc/keccak_absorb/Makefile b/proofs/cbmc/keccak_absorb/Makefile index 8fdd77ed96..89827d1698 100644 --- a/proofs/cbmc/keccak_absorb/Makefile +++ b/proofs/cbmc/keccak_absorb/Makefile @@ -29,7 +29,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:cvc5_arrays_exp CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = keccak_absorb diff --git a/proofs/cbmc/keccak_absorb_once_x4/Makefile b/proofs/cbmc/keccak_absorb_once_x4/Makefile index 24f412a84e..2e2352c9a1 100644 --- a/proofs/cbmc/keccak_absorb_once_x4/Makefile +++ b/proofs/cbmc/keccak_absorb_once_x4/Makefile @@ -27,7 +27,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:bitwuzla +CBMC_SUPPORTED_CONFIGS = \ + LP64:bitwuzla \ + LP64:cvc5_arrays_exp CBMC_DEFAULT_CONFIG = LP64:bitwuzla FUNCTION_NAME = mld_keccak_absorb_once_x4 diff --git a/proofs/cbmc/keccak_f1600_x1_native_aarch64/Makefile b/proofs/cbmc/keccak_f1600_x1_native_aarch64/Makefile index f7606102b7..ba0aac57de 100644 --- a/proofs/cbmc/keccak_f1600_x1_native_aarch64/Makefile +++ b/proofs/cbmc/keccak_f1600_x1_native_aarch64/Makefile @@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:bitwuzla +CBMC_SUPPORTED_CONFIGS = \ + LP64:bitwuzla \ + LP64:z3_no_bv_extract CBMC_DEFAULT_CONFIG = LP64:bitwuzla FUNCTION_NAME = keccak_f1600_x1_native diff --git a/proofs/cbmc/keccak_f1600_x1_native_aarch64_v84a/Makefile b/proofs/cbmc/keccak_f1600_x1_native_aarch64_v84a/Makefile index 5fe224423b..122b52dcb1 100644 --- a/proofs/cbmc/keccak_f1600_x1_native_aarch64_v84a/Makefile +++ b/proofs/cbmc/keccak_f1600_x1_native_aarch64_v84a/Makefile @@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:bitwuzla +CBMC_SUPPORTED_CONFIGS = \ + LP64:bitwuzla \ + LP64:cvc5_arrays_exp CBMC_DEFAULT_CONFIG = LP64:bitwuzla FUNCTION_NAME = keccak_f1600_x1_native diff --git a/proofs/cbmc/keccak_f1600_x4_native_aarch64_v84a/Makefile b/proofs/cbmc/keccak_f1600_x4_native_aarch64_v84a/Makefile index 32ee55f133..42e3661ca4 100644 --- a/proofs/cbmc/keccak_f1600_x4_native_aarch64_v84a/Makefile +++ b/proofs/cbmc/keccak_f1600_x4_native_aarch64_v84a/Makefile @@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:bitwuzla +CBMC_SUPPORTED_CONFIGS = \ + LP64:bitwuzla \ + LP64:z3 CBMC_DEFAULT_CONFIG = LP64:bitwuzla FUNCTION_NAME = keccak_f1600_x4_native_aarch64_v84a diff --git a/proofs/cbmc/keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid/Makefile b/proofs/cbmc/keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid/Makefile index 44439a3ea4..d19b30165f 100644 --- a/proofs/cbmc/keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid/Makefile +++ b/proofs/cbmc/keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid/Makefile @@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:bitwuzla +CBMC_SUPPORTED_CONFIGS = \ + LP64:bitwuzla \ + LP64:z3_smt_only CBMC_DEFAULT_CONFIG = LP64:bitwuzla FUNCTION_NAME = keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid diff --git a/proofs/cbmc/keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid/Makefile b/proofs/cbmc/keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid/Makefile index de49285598..42f4ed7453 100644 --- a/proofs/cbmc/keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid/Makefile +++ b/proofs/cbmc/keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid/Makefile @@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:bitwuzla +CBMC_SUPPORTED_CONFIGS = \ + LP64:bitwuzla \ + LP64:z3_smt_only CBMC_DEFAULT_CONFIG = LP64:bitwuzla FUNCTION_NAME = keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid diff --git a/proofs/cbmc/keccak_f1600_x4_native_avx2/Makefile b/proofs/cbmc/keccak_f1600_x4_native_avx2/Makefile index b30af2a3fb..416425406a 100644 --- a/proofs/cbmc/keccak_f1600_x4_native_avx2/Makefile +++ b/proofs/cbmc/keccak_f1600_x4_native_avx2/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:bitwuzla +CBMC_SUPPORTED_CONFIGS = \ + LP64:bitwuzla \ + LP64:cvc5_arrays_exp CBMC_DEFAULT_CONFIG = LP64:bitwuzla FUNCTION_NAME = keccak_f1600_x4_native_avx2 diff --git a/proofs/cbmc/keccak_finalize/Makefile b/proofs/cbmc/keccak_finalize/Makefile index a70ca5ed29..3b06fa1799 100644 --- a/proofs/cbmc/keccak_finalize/Makefile +++ b/proofs/cbmc/keccak_finalize/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:cvc5_arrays_exp CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = keccak_finalize diff --git a/proofs/cbmc/keccak_init/Makefile b/proofs/cbmc/keccak_init/Makefile index a1a6e96fdb..1691e0ee4b 100644 --- a/proofs/cbmc/keccak_init/Makefile +++ b/proofs/cbmc/keccak_init/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = keccak_init diff --git a/proofs/cbmc/keccak_squeeze/Makefile b/proofs/cbmc/keccak_squeeze/Makefile index 84e9b75fb0..2711a7a369 100644 --- a/proofs/cbmc/keccak_squeeze/Makefile +++ b/proofs/cbmc/keccak_squeeze/Makefile @@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:bitwuzla +CBMC_SUPPORTED_CONFIGS = \ + LP64:bitwuzla \ + LP64:z3 CBMC_DEFAULT_CONFIG = LP64:bitwuzla FUNCTION_NAME = keccak_squeeze diff --git a/proofs/cbmc/keccak_squeezeblocks_x4/Makefile b/proofs/cbmc/keccak_squeezeblocks_x4/Makefile index 24d594e152..59c5cb4446 100644 --- a/proofs/cbmc/keccak_squeezeblocks_x4/Makefile +++ b/proofs/cbmc/keccak_squeezeblocks_x4/Makefile @@ -27,7 +27,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:bitwuzla +CBMC_SUPPORTED_CONFIGS = \ + LP64:bitwuzla \ + LP64:z3 CBMC_DEFAULT_CONFIG = LP64:bitwuzla FUNCTION_NAME = mld_keccak_squeezeblocks_x4 diff --git a/proofs/cbmc/keccakf1600_extract_bytes/Makefile b/proofs/cbmc/keccakf1600_extract_bytes/Makefile index ed57bcaf4d..8326cf57af 100644 --- a/proofs/cbmc/keccakf1600_extract_bytes/Makefile +++ b/proofs/cbmc/keccakf1600_extract_bytes/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = mld_keccakf1600_extract_bytes diff --git a/proofs/cbmc/keccakf1600_extract_bytes_BE/Makefile b/proofs/cbmc/keccakf1600_extract_bytes_BE/Makefile index 35632c6962..bd5b8ae73c 100644 --- a/proofs/cbmc/keccakf1600_extract_bytes_BE/Makefile +++ b/proofs/cbmc/keccakf1600_extract_bytes_BE/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:cvc5_arrays_exp CBMC_DEFAULT_CONFIG = LP64:z3 CBMC_CONFIG_FLAGS = --big-endian diff --git a/proofs/cbmc/keccakf1600_permute/Makefile b/proofs/cbmc/keccakf1600_permute/Makefile index 14a96e168a..fc026c17f0 100644 --- a/proofs/cbmc/keccakf1600_permute/Makefile +++ b/proofs/cbmc/keccakf1600_permute/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = mld_keccakf1600_permute diff --git a/proofs/cbmc/keccakf1600_permute_c/Makefile b/proofs/cbmc/keccakf1600_permute_c/Makefile index 4928a0b9bc..98f392d3d5 100644 --- a/proofs/cbmc/keccakf1600_permute_c/Makefile +++ b/proofs/cbmc/keccakf1600_permute_c/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:cvc5_arrays_exp CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = mld_keccakf1600_permute_c diff --git a/proofs/cbmc/keccakf1600_permute_native/Makefile b/proofs/cbmc/keccakf1600_permute_native/Makefile index 70c79a0943..73e80f5ac1 100644 --- a/proofs/cbmc/keccakf1600_permute_native/Makefile +++ b/proofs/cbmc/keccakf1600_permute_native/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = mld_keccakf1600_permute_native diff --git a/proofs/cbmc/keccakf1600_xor_bytes/Makefile b/proofs/cbmc/keccakf1600_xor_bytes/Makefile index 70258277cd..1833bb7ee4 100644 --- a/proofs/cbmc/keccakf1600_xor_bytes/Makefile +++ b/proofs/cbmc/keccakf1600_xor_bytes/Makefile @@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:bitwuzla +CBMC_SUPPORTED_CONFIGS = \ + LP64:bitwuzla \ + LP64:cvc5_arrays_exp CBMC_DEFAULT_CONFIG = LP64:bitwuzla FUNCTION_NAME = mld_keccakf1600_xor_bytes diff --git a/proofs/cbmc/keccakf1600_xor_bytes_BE/Makefile b/proofs/cbmc/keccakf1600_xor_bytes_BE/Makefile index 08b46af8fe..e27d2d74c4 100644 --- a/proofs/cbmc/keccakf1600_xor_bytes_BE/Makefile +++ b/proofs/cbmc/keccakf1600_xor_bytes_BE/Makefile @@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:bitwuzla +CBMC_SUPPORTED_CONFIGS = \ + LP64:bitwuzla \ + LP64:z3_smt_only CBMC_DEFAULT_CONFIG = LP64:bitwuzla CBMC_CONFIG_FLAGS = --big-endian diff --git a/proofs/cbmc/keccakf1600x4_extract_bytes/Makefile b/proofs/cbmc/keccakf1600x4_extract_bytes/Makefile index 8693912a6d..06b4d70ec9 100644 --- a/proofs/cbmc/keccakf1600x4_extract_bytes/Makefile +++ b/proofs/cbmc/keccakf1600x4_extract_bytes/Makefile @@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:bitwuzla +CBMC_SUPPORTED_CONFIGS = \ + LP64:bitwuzla \ + LP64:z3 CBMC_DEFAULT_CONFIG = LP64:bitwuzla FUNCTION_NAME = mld_keccakf1600x4_extract_bytes diff --git a/proofs/cbmc/keccakf1600x4_extract_bytes_c/Makefile b/proofs/cbmc/keccakf1600x4_extract_bytes_c/Makefile index efe284965e..c30267d53a 100644 --- a/proofs/cbmc/keccakf1600x4_extract_bytes_c/Makefile +++ b/proofs/cbmc/keccakf1600x4_extract_bytes_c/Makefile @@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:cvc5_arrays_exp CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = mld_keccakf1600x4_extract_bytes_c diff --git a/proofs/cbmc/keccakf1600x4_extract_bytes_native/Makefile b/proofs/cbmc/keccakf1600x4_extract_bytes_native/Makefile index 6ddea667ee..a01bd9f612 100644 --- a/proofs/cbmc/keccakf1600x4_extract_bytes_native/Makefile +++ b/proofs/cbmc/keccakf1600x4_extract_bytes_native/Makefile @@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:bitwuzla +CBMC_SUPPORTED_CONFIGS = \ + LP64:bitwuzla \ + LP64:z3 CBMC_DEFAULT_CONFIG = LP64:bitwuzla FUNCTION_NAME = keccakf1600x4_extract_bytes_native diff --git a/proofs/cbmc/keccakf1600x4_permute/Makefile b/proofs/cbmc/keccakf1600x4_permute/Makefile index 081e646888..ce8393ee9f 100644 --- a/proofs/cbmc/keccakf1600x4_permute/Makefile +++ b/proofs/cbmc/keccakf1600x4_permute/Makefile @@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:cvc5_arrays_exp CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = mld_keccakf1600x4_permute diff --git a/proofs/cbmc/keccakf1600x4_permute_native/Makefile b/proofs/cbmc/keccakf1600x4_permute_native/Makefile index 56b7c9c713..3c9967d6b5 100644 --- a/proofs/cbmc/keccakf1600x4_permute_native/Makefile +++ b/proofs/cbmc/keccakf1600x4_permute_native/Makefile @@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:cvc5_arrays_exp CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = mld_keccakf1600x4_permute_native diff --git a/proofs/cbmc/keccakf1600x4_xor_bytes/Makefile b/proofs/cbmc/keccakf1600x4_xor_bytes/Makefile index 1f4dfaf577..9a59c5f355 100644 --- a/proofs/cbmc/keccakf1600x4_xor_bytes/Makefile +++ b/proofs/cbmc/keccakf1600x4_xor_bytes/Makefile @@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:bitwuzla +CBMC_SUPPORTED_CONFIGS = \ + LP64:bitwuzla \ + LP64:cvc5_arrays_exp CBMC_DEFAULT_CONFIG = LP64:bitwuzla FUNCTION_NAME = mld_keccakf1600x4_xor_bytes diff --git a/proofs/cbmc/keccakf1600x4_xor_bytes_c/Makefile b/proofs/cbmc/keccakf1600x4_xor_bytes_c/Makefile index 1d741d50a5..7eb05ba502 100644 --- a/proofs/cbmc/keccakf1600x4_xor_bytes_c/Makefile +++ b/proofs/cbmc/keccakf1600x4_xor_bytes_c/Makefile @@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = mld_keccakf1600x4_xor_bytes_c diff --git a/proofs/cbmc/keccakf1600x4_xor_bytes_native/Makefile b/proofs/cbmc/keccakf1600x4_xor_bytes_native/Makefile index 64ac591070..1e0851a3e5 100644 --- a/proofs/cbmc/keccakf1600x4_xor_bytes_native/Makefile +++ b/proofs/cbmc/keccakf1600x4_xor_bytes_native/Makefile @@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:bitwuzla +CBMC_SUPPORTED_CONFIGS = \ + LP64:bitwuzla \ + LP64:z3_no_bv_extract CBMC_DEFAULT_CONFIG = LP64:bitwuzla FUNCTION_NAME = keccakf1600x4_xor_bytes_native diff --git a/proofs/cbmc/make_hint/Makefile b/proofs/cbmc/make_hint/Makefile index 2c3c3f3b4a..dfe1508fee 100644 --- a/proofs/cbmc/make_hint/Makefile +++ b/proofs/cbmc/make_hint/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:cvc5_arrays_exp CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = make_hint diff --git a/proofs/cbmc/montgomery_reduce/Makefile b/proofs/cbmc/montgomery_reduce/Makefile index a45d198037..9d01383c01 100644 --- a/proofs/cbmc/montgomery_reduce/Makefile +++ b/proofs/cbmc/montgomery_reduce/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:cvc5_arrays_exp CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = montgomery_reduce diff --git a/proofs/cbmc/ntt_layer/Makefile b/proofs/cbmc/ntt_layer/Makefile index 60d3ed2347..83db1423e1 100644 --- a/proofs/cbmc/ntt_layer/Makefile +++ b/proofs/cbmc/ntt_layer/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:bitwuzla +CBMC_SUPPORTED_CONFIGS = \ + LP64:bitwuzla \ + LP64:z3_no_bv_extract CBMC_DEFAULT_CONFIG = LP64:bitwuzla FUNCTION_NAME = mld_ntt_layer diff --git a/proofs/cbmc/ntt_native_aarch64/Makefile b/proofs/cbmc/ntt_native_aarch64/Makefile index 603df251ac..aa56504f95 100644 --- a/proofs/cbmc/ntt_native_aarch64/Makefile +++ b/proofs/cbmc/ntt_native_aarch64/Makefile @@ -28,7 +28,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = ntt_native_aarch64 diff --git a/proofs/cbmc/ntt_native_x86_64/Makefile b/proofs/cbmc/ntt_native_x86_64/Makefile index fbd5bc9216..546395a564 100644 --- a/proofs/cbmc/ntt_native_x86_64/Makefile +++ b/proofs/cbmc/ntt_native_x86_64/Makefile @@ -28,7 +28,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = ntt_native_x86_64 diff --git a/proofs/cbmc/pack_sig_c/Makefile b/proofs/cbmc/pack_sig_c/Makefile index 685392e09d..bf23331214 100644 --- a/proofs/cbmc/pack_sig_c/Makefile +++ b/proofs/cbmc/pack_sig_c/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:cvc5_arrays_exp CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = pack_sig_c diff --git a/proofs/cbmc/pack_sig_h/Makefile b/proofs/cbmc/pack_sig_h/Makefile index 11961ad74a..9c8b9bd3f4 100644 --- a/proofs/cbmc/pack_sig_h/Makefile +++ b/proofs/cbmc/pack_sig_h/Makefile @@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3_no_bv_extract +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3_no_bv_extract \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3_no_bv_extract FUNCTION_NAME = pack_sig_h diff --git a/proofs/cbmc/pack_sig_z/Makefile b/proofs/cbmc/pack_sig_z/Makefile index 133b6523c8..61db9495e5 100644 --- a/proofs/cbmc/pack_sig_z/Makefile +++ b/proofs/cbmc/pack_sig_z/Makefile @@ -24,7 +24,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = pack_sig_z diff --git a/proofs/cbmc/pack_sk_rho_key_tr/Makefile b/proofs/cbmc/pack_sk_rho_key_tr/Makefile index db18d4d31d..86306887d4 100644 --- a/proofs/cbmc/pack_sk_rho_key_tr/Makefile +++ b/proofs/cbmc/pack_sk_rho_key_tr/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = pack_sk_rho_key_tr diff --git a/proofs/cbmc/pointwise_native_aarch64/Makefile b/proofs/cbmc/pointwise_native_aarch64/Makefile index e6ca095b06..f606f692a2 100644 --- a/proofs/cbmc/pointwise_native_aarch64/Makefile +++ b/proofs/cbmc/pointwise_native_aarch64/Makefile @@ -28,7 +28,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = pointwise_native_aarch64 diff --git a/proofs/cbmc/pointwise_native_x86_64/Makefile b/proofs/cbmc/pointwise_native_x86_64/Makefile index ab74386f0c..f79638ac6c 100644 --- a/proofs/cbmc/pointwise_native_x86_64/Makefile +++ b/proofs/cbmc/pointwise_native_x86_64/Makefile @@ -28,7 +28,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = pointwise_native_x86_64 diff --git a/proofs/cbmc/poly_caddq/Makefile b/proofs/cbmc/poly_caddq/Makefile index 13c1a552a3..d37188ac3d 100644 --- a/proofs/cbmc/poly_caddq/Makefile +++ b/proofs/cbmc/poly_caddq/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = poly_caddq diff --git a/proofs/cbmc/poly_caddq_c/Makefile b/proofs/cbmc/poly_caddq_c/Makefile index 5584a20f5b..303f76f153 100644 --- a/proofs/cbmc/poly_caddq_c/Makefile +++ b/proofs/cbmc/poly_caddq_c/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = mld_poly_caddq_c diff --git a/proofs/cbmc/poly_caddq_native/Makefile b/proofs/cbmc/poly_caddq_native/Makefile index 4cbe66e36d..173817355f 100644 --- a/proofs/cbmc/poly_caddq_native/Makefile +++ b/proofs/cbmc/poly_caddq_native/Makefile @@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = poly_caddq_native diff --git a/proofs/cbmc/poly_caddq_native_x86_64/Makefile b/proofs/cbmc/poly_caddq_native_x86_64/Makefile index 6dbfb50395..1d494fcfd7 100644 --- a/proofs/cbmc/poly_caddq_native_x86_64/Makefile +++ b/proofs/cbmc/poly_caddq_native_x86_64/Makefile @@ -28,7 +28,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = poly_caddq_native_x86_64 diff --git a/proofs/cbmc/poly_challenge/Makefile b/proofs/cbmc/poly_challenge/Makefile index c0b0e4ecc9..83a6b83313 100644 --- a/proofs/cbmc/poly_challenge/Makefile +++ b/proofs/cbmc/poly_challenge/Makefile @@ -30,7 +30,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = poly_challenge diff --git a/proofs/cbmc/poly_chknorm/Makefile b/proofs/cbmc/poly_chknorm/Makefile index a4dc23b138..576cb24644 100644 --- a/proofs/cbmc/poly_chknorm/Makefile +++ b/proofs/cbmc/poly_chknorm/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = poly_chknorm diff --git a/proofs/cbmc/poly_chknorm_c/Makefile b/proofs/cbmc/poly_chknorm_c/Makefile index 64c9c1b5f8..462b35cb42 100644 --- a/proofs/cbmc/poly_chknorm_c/Makefile +++ b/proofs/cbmc/poly_chknorm_c/Makefile @@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = mld_poly_chknorm_c diff --git a/proofs/cbmc/poly_chknorm_native/Makefile b/proofs/cbmc/poly_chknorm_native/Makefile index b89ba6297f..a05bfbb85a 100644 --- a/proofs/cbmc/poly_chknorm_native/Makefile +++ b/proofs/cbmc/poly_chknorm_native/Makefile @@ -27,7 +27,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = poly_chknorm_native diff --git a/proofs/cbmc/poly_chknorm_native_aarch64/Makefile b/proofs/cbmc/poly_chknorm_native_aarch64/Makefile index 800f6d222f..b15e8e25fe 100644 --- a/proofs/cbmc/poly_chknorm_native_aarch64/Makefile +++ b/proofs/cbmc/poly_chknorm_native_aarch64/Makefile @@ -28,7 +28,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = poly_chknorm_native_aarch64 diff --git a/proofs/cbmc/poly_chknorm_native_x86_64/Makefile b/proofs/cbmc/poly_chknorm_native_x86_64/Makefile index bbc0b8de4c..7b1aebde75 100644 --- a/proofs/cbmc/poly_chknorm_native_x86_64/Makefile +++ b/proofs/cbmc/poly_chknorm_native_x86_64/Makefile @@ -28,7 +28,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = poly_chknorm_native_x86_64 diff --git a/proofs/cbmc/poly_decompose/Makefile b/proofs/cbmc/poly_decompose/Makefile index 1247f331e0..926e8508ae 100644 --- a/proofs/cbmc/poly_decompose/Makefile +++ b/proofs/cbmc/poly_decompose/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = poly_decompose diff --git a/proofs/cbmc/poly_decompose_88_native_aarch64/Makefile b/proofs/cbmc/poly_decompose_88_native_aarch64/Makefile index 28dc99c219..ee608a6ec3 100644 --- a/proofs/cbmc/poly_decompose_88_native_aarch64/Makefile +++ b/proofs/cbmc/poly_decompose_88_native_aarch64/Makefile @@ -33,7 +33,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = poly_decompose_88_native_aarch64 diff --git a/proofs/cbmc/poly_invntt_tomont/Makefile b/proofs/cbmc/poly_invntt_tomont/Makefile index afb6295d49..206f380ca0 100644 --- a/proofs/cbmc/poly_invntt_tomont/Makefile +++ b/proofs/cbmc/poly_invntt_tomont/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = poly_invntt_tomont diff --git a/proofs/cbmc/poly_invntt_tomont_native/Makefile b/proofs/cbmc/poly_invntt_tomont_native/Makefile index 145f0e3e7e..c0432732be 100644 --- a/proofs/cbmc/poly_invntt_tomont_native/Makefile +++ b/proofs/cbmc/poly_invntt_tomont_native/Makefile @@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = poly_invntt_tomont_native diff --git a/proofs/cbmc/poly_ntt/Makefile b/proofs/cbmc/poly_ntt/Makefile index 6b01a7d061..67a26c5d18 100644 --- a/proofs/cbmc/poly_ntt/Makefile +++ b/proofs/cbmc/poly_ntt/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = poly_ntt diff --git a/proofs/cbmc/poly_ntt_c/Makefile b/proofs/cbmc/poly_ntt_c/Makefile index 4ea1f27f16..21dbc5e873 100644 --- a/proofs/cbmc/poly_ntt_c/Makefile +++ b/proofs/cbmc/poly_ntt_c/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3_smt_only +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3_smt_only \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3_smt_only FUNCTION_NAME = mld_poly_ntt_c diff --git a/proofs/cbmc/poly_ntt_native/Makefile b/proofs/cbmc/poly_ntt_native/Makefile index 3abe9084a0..0159d387bd 100644 --- a/proofs/cbmc/poly_ntt_native/Makefile +++ b/proofs/cbmc/poly_ntt_native/Makefile @@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = poly_ntt diff --git a/proofs/cbmc/poly_permute_bitrev_to_custom_optional/Makefile b/proofs/cbmc/poly_permute_bitrev_to_custom_optional/Makefile index a67d113f27..9c489ea99e 100644 --- a/proofs/cbmc/poly_permute_bitrev_to_custom_optional/Makefile +++ b/proofs/cbmc/poly_permute_bitrev_to_custom_optional/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = poly_permute_bitrev_to_custom_optional diff --git a/proofs/cbmc/poly_permute_bitrev_to_custom_optional_native/Makefile b/proofs/cbmc/poly_permute_bitrev_to_custom_optional_native/Makefile index 56e455b3b4..8e745b8dd1 100644 --- a/proofs/cbmc/poly_permute_bitrev_to_custom_optional_native/Makefile +++ b/proofs/cbmc/poly_permute_bitrev_to_custom_optional_native/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = poly_permute_bitrev_to_custom_optional_native diff --git a/proofs/cbmc/poly_pointwise_montgomery/Makefile b/proofs/cbmc/poly_pointwise_montgomery/Makefile index 041f7c1ace..469720ed7f 100644 --- a/proofs/cbmc/poly_pointwise_montgomery/Makefile +++ b/proofs/cbmc/poly_pointwise_montgomery/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = poly_pointwise_montgomery diff --git a/proofs/cbmc/poly_reduce/Makefile b/proofs/cbmc/poly_reduce/Makefile index f3b398c89e..f680b1dbb8 100644 --- a/proofs/cbmc/poly_reduce/Makefile +++ b/proofs/cbmc/poly_reduce/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = poly_reduce diff --git a/proofs/cbmc/poly_shiftl/Makefile b/proofs/cbmc/poly_shiftl/Makefile index 371125e38a..7127ab41af 100644 --- a/proofs/cbmc/poly_shiftl/Makefile +++ b/proofs/cbmc/poly_shiftl/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = poly_shiftl diff --git a/proofs/cbmc/poly_sub/Makefile b/proofs/cbmc/poly_sub/Makefile index 18c301c1ee..450a01120f 100644 --- a/proofs/cbmc/poly_sub/Makefile +++ b/proofs/cbmc/poly_sub/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = poly_sub diff --git a/proofs/cbmc/poly_use_hint_native_aarch64/Makefile b/proofs/cbmc/poly_use_hint_native_aarch64/Makefile index 3f06d3fef7..274dbc4906 100644 --- a/proofs/cbmc/poly_use_hint_native_aarch64/Makefile +++ b/proofs/cbmc/poly_use_hint_native_aarch64/Makefile @@ -36,7 +36,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = poly_use_hint_native_aarch64 diff --git a/proofs/cbmc/poly_use_hint_native_x86_64/Makefile b/proofs/cbmc/poly_use_hint_native_x86_64/Makefile index e02a7eef9e..6cf9a38102 100644 --- a/proofs/cbmc/poly_use_hint_native_x86_64/Makefile +++ b/proofs/cbmc/poly_use_hint_native_x86_64/Makefile @@ -38,7 +38,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = poly_use_hint_native_x86_64 diff --git a/proofs/cbmc/polyeta_pack/Makefile b/proofs/cbmc/polyeta_pack/Makefile index f2d00f8a95..38f38d8a62 100644 --- a/proofs/cbmc/polyeta_pack/Makefile +++ b/proofs/cbmc/polyeta_pack/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = polyeta_pack diff --git a/proofs/cbmc/polyeta_unpack/Makefile b/proofs/cbmc/polyeta_unpack/Makefile index ae278b6780..0ad1d5a8a4 100644 --- a/proofs/cbmc/polyeta_unpack/Makefile +++ b/proofs/cbmc/polyeta_unpack/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = polyeta_unpack diff --git a/proofs/cbmc/polymat_expand_entry/Makefile b/proofs/cbmc/polymat_expand_entry/Makefile index dcf37ea9a5..85fe9bce19 100644 --- a/proofs/cbmc/polymat_expand_entry/Makefile +++ b/proofs/cbmc/polymat_expand_entry/Makefile @@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = mld_polymat_expand_entry diff --git a/proofs/cbmc/polyt0_pack/Makefile b/proofs/cbmc/polyt0_pack/Makefile index 9467df269c..5986ca0b69 100644 --- a/proofs/cbmc/polyt0_pack/Makefile +++ b/proofs/cbmc/polyt0_pack/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = polyt0_pack diff --git a/proofs/cbmc/polyt0_unpack/Makefile b/proofs/cbmc/polyt0_unpack/Makefile index 54e57406c5..23a838588d 100644 --- a/proofs/cbmc/polyt0_unpack/Makefile +++ b/proofs/cbmc/polyt0_unpack/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = polyt0_unpack diff --git a/proofs/cbmc/polyt1_pack/Makefile b/proofs/cbmc/polyt1_pack/Makefile index 6149c46dd5..1e1aa5ce7a 100644 --- a/proofs/cbmc/polyt1_pack/Makefile +++ b/proofs/cbmc/polyt1_pack/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = polyt1_pack diff --git a/proofs/cbmc/polyt1_unpack/Makefile b/proofs/cbmc/polyt1_unpack/Makefile index 88bf8478c7..25f5d34684 100644 --- a/proofs/cbmc/polyt1_unpack/Makefile +++ b/proofs/cbmc/polyt1_unpack/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = polyt1_unpack diff --git a/proofs/cbmc/polyw1_pack/Makefile b/proofs/cbmc/polyw1_pack/Makefile index 13e9eba90d..7fe5125c71 100644 --- a/proofs/cbmc/polyw1_pack/Makefile +++ b/proofs/cbmc/polyw1_pack/Makefile @@ -29,7 +29,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = polyw1_pack diff --git a/proofs/cbmc/polyw1_pack_32/Makefile b/proofs/cbmc/polyw1_pack_32/Makefile index 8a26b4f190..57a2ecef8c 100644 --- a/proofs/cbmc/polyw1_pack_32/Makefile +++ b/proofs/cbmc/polyw1_pack_32/Makefile @@ -29,7 +29,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = polyw1_pack_32 diff --git a/proofs/cbmc/polyw1_pack_88/Makefile b/proofs/cbmc/polyw1_pack_88/Makefile index 6db568775c..798d8c2c7b 100644 --- a/proofs/cbmc/polyw1_pack_88/Makefile +++ b/proofs/cbmc/polyw1_pack_88/Makefile @@ -29,7 +29,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = polyw1_pack_88 diff --git a/proofs/cbmc/polyw1_unpack/Makefile b/proofs/cbmc/polyw1_unpack/Makefile index 475735daff..aff7e6cd04 100644 --- a/proofs/cbmc/polyw1_unpack/Makefile +++ b/proofs/cbmc/polyw1_unpack/Makefile @@ -29,7 +29,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = polyw1_unpack diff --git a/proofs/cbmc/polyw1_unpack_32/Makefile b/proofs/cbmc/polyw1_unpack_32/Makefile index ffc9335a4b..95aef46f0c 100644 --- a/proofs/cbmc/polyw1_unpack_32/Makefile +++ b/proofs/cbmc/polyw1_unpack_32/Makefile @@ -29,7 +29,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = polyw1_unpack_32 diff --git a/proofs/cbmc/polyw1_unpack_88/Makefile b/proofs/cbmc/polyw1_unpack_88/Makefile index 15b14f3ace..465b1ce327 100644 --- a/proofs/cbmc/polyw1_unpack_88/Makefile +++ b/proofs/cbmc/polyw1_unpack_88/Makefile @@ -29,7 +29,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = polyw1_unpack_88 diff --git a/proofs/cbmc/polyz_pack/Makefile b/proofs/cbmc/polyz_pack/Makefile index 40774b3ca8..f62d66df7f 100644 --- a/proofs/cbmc/polyz_pack/Makefile +++ b/proofs/cbmc/polyz_pack/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = polyz_pack diff --git a/proofs/cbmc/polyz_unpack/Makefile b/proofs/cbmc/polyz_unpack/Makefile index 2574eed6cc..319204ce3f 100644 --- a/proofs/cbmc/polyz_unpack/Makefile +++ b/proofs/cbmc/polyz_unpack/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = polyz_unpack diff --git a/proofs/cbmc/polyz_unpack_17_native_aarch64/Makefile b/proofs/cbmc/polyz_unpack_17_native_aarch64/Makefile index 049148a90b..5dbcf155d2 100644 --- a/proofs/cbmc/polyz_unpack_17_native_aarch64/Makefile +++ b/proofs/cbmc/polyz_unpack_17_native_aarch64/Makefile @@ -33,7 +33,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = polyz_unpack_17_native_aarch64 diff --git a/proofs/cbmc/polyz_unpack_19_native_aarch64/Makefile b/proofs/cbmc/polyz_unpack_19_native_aarch64/Makefile index e97c20f955..3117f348dd 100644 --- a/proofs/cbmc/polyz_unpack_19_native_aarch64/Makefile +++ b/proofs/cbmc/polyz_unpack_19_native_aarch64/Makefile @@ -36,7 +36,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = polyz_unpack_19_native_aarch64 diff --git a/proofs/cbmc/polyz_unpack_c/Makefile b/proofs/cbmc/polyz_unpack_c/Makefile index 4c31676a04..d639b0b2a9 100644 --- a/proofs/cbmc/polyz_unpack_c/Makefile +++ b/proofs/cbmc/polyz_unpack_c/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = mld_polyz_unpack_c diff --git a/proofs/cbmc/polyz_unpack_native/Makefile b/proofs/cbmc/polyz_unpack_native/Makefile index c21edffef2..a7f802ce12 100644 --- a/proofs/cbmc/polyz_unpack_native/Makefile +++ b/proofs/cbmc/polyz_unpack_native/Makefile @@ -32,7 +32,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = polyz_unpack_native diff --git a/proofs/cbmc/polyz_unpack_native_x86_64/Makefile b/proofs/cbmc/polyz_unpack_native_x86_64/Makefile index 15cbe9cdf2..5bbfbd5c67 100644 --- a/proofs/cbmc/polyz_unpack_native_x86_64/Makefile +++ b/proofs/cbmc/polyz_unpack_native_x86_64/Makefile @@ -38,7 +38,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = polyz_unpack_native_x86_64 diff --git a/proofs/cbmc/power2round/Makefile b/proofs/cbmc/power2round/Makefile index cb93062e23..13144776bd 100644 --- a/proofs/cbmc/power2round/Makefile +++ b/proofs/cbmc/power2round/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = power2round diff --git a/proofs/cbmc/prepare_domain_separation_prefix/Makefile b/proofs/cbmc/prepare_domain_separation_prefix/Makefile index dc8d89e70b..0226e24ee0 100644 --- a/proofs/cbmc/prepare_domain_separation_prefix/Makefile +++ b/proofs/cbmc/prepare_domain_separation_prefix/Makefile @@ -25,7 +25,9 @@ USE_DYNAMIC_FRAMES=1 FUNCTION_NAME = prepare_domain_separation_prefix # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 CBMC_OBJECT_BITS = 8 diff --git a/proofs/cbmc/reduce32/Makefile b/proofs/cbmc/reduce32/Makefile index 14b2b706d4..2d43e0f1c4 100644 --- a/proofs/cbmc/reduce32/Makefile +++ b/proofs/cbmc/reduce32/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = reduce32 diff --git a/proofs/cbmc/rej_eta/Makefile b/proofs/cbmc/rej_eta/Makefile index fad9384ee7..4183b503b0 100644 --- a/proofs/cbmc/rej_eta/Makefile +++ b/proofs/cbmc/rej_eta/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:bitwuzla +CBMC_SUPPORTED_CONFIGS = \ + LP64:bitwuzla \ + LP64:z3_smt_only CBMC_DEFAULT_CONFIG = LP64:bitwuzla FUNCTION_NAME = mld_rej_eta diff --git a/proofs/cbmc/rej_eta_c/Makefile b/proofs/cbmc/rej_eta_c/Makefile index 688379e620..3664417ad0 100644 --- a/proofs/cbmc/rej_eta_c/Makefile +++ b/proofs/cbmc/rej_eta_c/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:bitwuzla +CBMC_SUPPORTED_CONFIGS = \ + LP64:bitwuzla \ + LP64:z3 CBMC_DEFAULT_CONFIG = LP64:bitwuzla FUNCTION_NAME = mld_rej_eta_c diff --git a/proofs/cbmc/rej_eta_native/Makefile b/proofs/cbmc/rej_eta_native/Makefile index 3b342a51d9..af2c7ddc02 100644 --- a/proofs/cbmc/rej_eta_native/Makefile +++ b/proofs/cbmc/rej_eta_native/Makefile @@ -32,7 +32,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:bitwuzla +CBMC_SUPPORTED_CONFIGS = \ + LP64:bitwuzla \ + LP64:z3_smt_only CBMC_DEFAULT_CONFIG = LP64:bitwuzla FUNCTION_NAME = mld_rej_eta_native diff --git a/proofs/cbmc/rej_uniform/Makefile b/proofs/cbmc/rej_uniform/Makefile index 77ccb5ddb4..993dd16a31 100644 --- a/proofs/cbmc/rej_uniform/Makefile +++ b/proofs/cbmc/rej_uniform/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = mld_rej_uniform diff --git a/proofs/cbmc/rej_uniform_c/Makefile b/proofs/cbmc/rej_uniform_c/Makefile index 2ca6da901e..931f05aadf 100644 --- a/proofs/cbmc/rej_uniform_c/Makefile +++ b/proofs/cbmc/rej_uniform_c/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = mld_rej_uniform_c diff --git a/proofs/cbmc/rej_uniform_eta_native_aarch64/Makefile b/proofs/cbmc/rej_uniform_eta_native_aarch64/Makefile index 77d3c930ee..3f465c6c6c 100644 --- a/proofs/cbmc/rej_uniform_eta_native_aarch64/Makefile +++ b/proofs/cbmc/rej_uniform_eta_native_aarch64/Makefile @@ -37,7 +37,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:bitwuzla +CBMC_SUPPORTED_CONFIGS = \ + LP64:bitwuzla \ + LP64:z3_smt_only CBMC_DEFAULT_CONFIG = LP64:bitwuzla FUNCTION_NAME = rej_uniform_eta_native_aarch64 diff --git a/proofs/cbmc/rej_uniform_eta_native_x86_64/Makefile b/proofs/cbmc/rej_uniform_eta_native_x86_64/Makefile index cb9044b1cf..3f6a33e434 100644 --- a/proofs/cbmc/rej_uniform_eta_native_x86_64/Makefile +++ b/proofs/cbmc/rej_uniform_eta_native_x86_64/Makefile @@ -37,7 +37,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3_smt_only +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3_smt_only \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3_smt_only FUNCTION_NAME = rej_uniform_eta_native_x86_64 diff --git a/proofs/cbmc/rej_uniform_native/Makefile b/proofs/cbmc/rej_uniform_native/Makefile index 3735881b8a..7572b9086a 100644 --- a/proofs/cbmc/rej_uniform_native/Makefile +++ b/proofs/cbmc/rej_uniform_native/Makefile @@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:bitwuzla +CBMC_SUPPORTED_CONFIGS = \ + LP64:bitwuzla \ + LP64:z3_smt_only CBMC_DEFAULT_CONFIG = LP64:bitwuzla FUNCTION_NAME = mld_rej_uniform_native_native diff --git a/proofs/cbmc/rej_uniform_native_aarch64/Makefile b/proofs/cbmc/rej_uniform_native_aarch64/Makefile index 7ba4529be6..d1c26eaf4b 100644 --- a/proofs/cbmc/rej_uniform_native_aarch64/Makefile +++ b/proofs/cbmc/rej_uniform_native_aarch64/Makefile @@ -27,7 +27,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:bitwuzla +CBMC_SUPPORTED_CONFIGS = \ + LP64:bitwuzla \ + LP64:z3_smt_only CBMC_DEFAULT_CONFIG = LP64:bitwuzla FUNCTION_NAME = rej_uniform_native_aarch64 diff --git a/proofs/cbmc/rej_uniform_native_x86_64/Makefile b/proofs/cbmc/rej_uniform_native_x86_64/Makefile index 620f3ea975..e4b5554a0e 100644 --- a/proofs/cbmc/rej_uniform_native_x86_64/Makefile +++ b/proofs/cbmc/rej_uniform_native_x86_64/Makefile @@ -30,7 +30,9 @@ USE_DYNAMIC_FRAMES=1 # straight to the SMT tactic) to avoid Z3 divergence in solve time across # platforms, which otherwise pushes this proof over the CI per-proof timeout. # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3_smt_only +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3_smt_only \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3_smt_only FUNCTION_NAME = rej_uniform_native_x86_64 diff --git a/proofs/cbmc/shake128_absorb/Makefile b/proofs/cbmc/shake128_absorb/Makefile index 684ca0691a..870451edfc 100644 --- a/proofs/cbmc/shake128_absorb/Makefile +++ b/proofs/cbmc/shake128_absorb/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:cvc5_arrays_exp CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = shake128_absorb diff --git a/proofs/cbmc/shake128_finalize/Makefile b/proofs/cbmc/shake128_finalize/Makefile index 2fd0e1ec75..75095f0f5c 100644 --- a/proofs/cbmc/shake128_finalize/Makefile +++ b/proofs/cbmc/shake128_finalize/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:cvc5_arrays_exp CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = shake128_finalize diff --git a/proofs/cbmc/shake128_init/Makefile b/proofs/cbmc/shake128_init/Makefile index 9c1e18becd..c756b43683 100644 --- a/proofs/cbmc/shake128_init/Makefile +++ b/proofs/cbmc/shake128_init/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = shake128_init diff --git a/proofs/cbmc/shake128_release/Makefile b/proofs/cbmc/shake128_release/Makefile index c65894c4fa..3e1504dbe3 100644 --- a/proofs/cbmc/shake128_release/Makefile +++ b/proofs/cbmc/shake128_release/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = shake128_release diff --git a/proofs/cbmc/shake128_squeeze/Makefile b/proofs/cbmc/shake128_squeeze/Makefile index 215db718b4..a75ca937c7 100644 --- a/proofs/cbmc/shake128_squeeze/Makefile +++ b/proofs/cbmc/shake128_squeeze/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:bitwuzla +CBMC_SUPPORTED_CONFIGS = \ + LP64:bitwuzla \ + LP64:cvc5_arrays_exp CBMC_DEFAULT_CONFIG = LP64:bitwuzla FUNCTION_NAME = shake128_squeeze diff --git a/proofs/cbmc/shake128x4_absorb_once/Makefile b/proofs/cbmc/shake128x4_absorb_once/Makefile index c1b0993744..08f1b89ef3 100644 --- a/proofs/cbmc/shake128x4_absorb_once/Makefile +++ b/proofs/cbmc/shake128x4_absorb_once/Makefile @@ -31,7 +31,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:bitwuzla +CBMC_SUPPORTED_CONFIGS = \ + LP64:bitwuzla \ + LP64:z3_smt_only CBMC_DEFAULT_CONFIG = LP64:bitwuzla FUNCTION_NAME = mld_shake128x4_absorb_once diff --git a/proofs/cbmc/shake128x4_squeezeblocks/Makefile b/proofs/cbmc/shake128x4_squeezeblocks/Makefile index 678c3245c1..1262550c92 100644 --- a/proofs/cbmc/shake128x4_squeezeblocks/Makefile +++ b/proofs/cbmc/shake128x4_squeezeblocks/Makefile @@ -31,7 +31,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:bitwuzla +CBMC_SUPPORTED_CONFIGS = \ + LP64:bitwuzla \ + LP64:z3 CBMC_DEFAULT_CONFIG = LP64:bitwuzla FUNCTION_NAME = mld_shake128x4_squeezeblocks diff --git a/proofs/cbmc/shake256/Makefile b/proofs/cbmc/shake256/Makefile index e65760e6cc..e23c9ebfa6 100644 --- a/proofs/cbmc/shake256/Makefile +++ b/proofs/cbmc/shake256/Makefile @@ -29,7 +29,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = shake256 diff --git a/proofs/cbmc/shake256_absorb/Makefile b/proofs/cbmc/shake256_absorb/Makefile index 0164017a7c..42b174ed8a 100644 --- a/proofs/cbmc/shake256_absorb/Makefile +++ b/proofs/cbmc/shake256_absorb/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = shake256_absorb diff --git a/proofs/cbmc/shake256_finalize/Makefile b/proofs/cbmc/shake256_finalize/Makefile index b92c23433e..7f3b89a7e1 100644 --- a/proofs/cbmc/shake256_finalize/Makefile +++ b/proofs/cbmc/shake256_finalize/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:cvc5_arrays_exp CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = shake256_finalize diff --git a/proofs/cbmc/shake256_init/Makefile b/proofs/cbmc/shake256_init/Makefile index a1ec98e203..aed98a08ff 100644 --- a/proofs/cbmc/shake256_init/Makefile +++ b/proofs/cbmc/shake256_init/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:cvc5_arrays_exp CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = shake256_init diff --git a/proofs/cbmc/shake256_release/Makefile b/proofs/cbmc/shake256_release/Makefile index 9bcc1d8569..1f3dc8d315 100644 --- a/proofs/cbmc/shake256_release/Makefile +++ b/proofs/cbmc/shake256_release/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = shake256_release diff --git a/proofs/cbmc/shake256_squeeze/Makefile b/proofs/cbmc/shake256_squeeze/Makefile index 8a99eb03ef..cfb51f9b08 100644 --- a/proofs/cbmc/shake256_squeeze/Makefile +++ b/proofs/cbmc/shake256_squeeze/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:bitwuzla +CBMC_SUPPORTED_CONFIGS = \ + LP64:bitwuzla \ + LP64:z3 CBMC_DEFAULT_CONFIG = LP64:bitwuzla FUNCTION_NAME = shake256_squeeze diff --git a/proofs/cbmc/shake256x4_absorb_once/Makefile b/proofs/cbmc/shake256x4_absorb_once/Makefile index a75f84d176..666b35b85e 100644 --- a/proofs/cbmc/shake256x4_absorb_once/Makefile +++ b/proofs/cbmc/shake256x4_absorb_once/Makefile @@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:bitwuzla +CBMC_SUPPORTED_CONFIGS = \ + LP64:bitwuzla \ + LP64:z3 CBMC_DEFAULT_CONFIG = LP64:bitwuzla FUNCTION_NAME = mld_shake256x4_absorb_once diff --git a/proofs/cbmc/shake256x4_squeezeblocks/Makefile b/proofs/cbmc/shake256x4_squeezeblocks/Makefile index 5fd68508f1..369376541c 100644 --- a/proofs/cbmc/shake256x4_squeezeblocks/Makefile +++ b/proofs/cbmc/shake256x4_squeezeblocks/Makefile @@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:bitwuzla +CBMC_SUPPORTED_CONFIGS = \ + LP64:bitwuzla \ + LP64:z3_smt_only CBMC_DEFAULT_CONFIG = LP64:bitwuzla FUNCTION_NAME = mld_shake256x4_squeezeblocks diff --git a/proofs/cbmc/sig_unpack_hints/Makefile b/proofs/cbmc/sig_unpack_hints/Makefile index 0343524607..68af5d9a27 100644 --- a/proofs/cbmc/sig_unpack_hints/Makefile +++ b/proofs/cbmc/sig_unpack_hints/Makefile @@ -24,7 +24,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = mld_sig_unpack_hints diff --git a/proofs/cbmc/sign_attempt/Makefile b/proofs/cbmc/sign_attempt/Makefile index c953a474f7..28ff211831 100644 --- a/proofs/cbmc/sign_attempt/Makefile +++ b/proofs/cbmc/sign_attempt/Makefile @@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:cvc5_arrays_exp CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = mld_sign_hook_attempt diff --git a/proofs/cbmc/sign_finish/Makefile b/proofs/cbmc/sign_finish/Makefile index f17ba0f219..98514cf019 100644 --- a/proofs/cbmc/sign_finish/Makefile +++ b/proofs/cbmc/sign_finish/Makefile @@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = mld_sign_hook_finish diff --git a/proofs/cbmc/sign_resume/Makefile b/proofs/cbmc/sign_resume/Makefile index a32cd0877d..728ae48149 100644 --- a/proofs/cbmc/sign_resume/Makefile +++ b/proofs/cbmc/sign_resume/Makefile @@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = mld_sign_hook_resume diff --git a/proofs/cbmc/sign_signature/Makefile b/proofs/cbmc/sign_signature/Makefile index 16222c01c5..1c0dc8062f 100644 --- a/proofs/cbmc/sign_signature/Makefile +++ b/proofs/cbmc/sign_signature/Makefile @@ -28,7 +28,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = sign_signature diff --git a/proofs/cbmc/sign_signature_pre_hash_internal/Makefile b/proofs/cbmc/sign_signature_pre_hash_internal/Makefile index aca2f51a36..83d8e0f188 100644 --- a/proofs/cbmc/sign_signature_pre_hash_internal/Makefile +++ b/proofs/cbmc/sign_signature_pre_hash_internal/Makefile @@ -27,7 +27,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = sign_signature_pre_hash_internal diff --git a/proofs/cbmc/sign_signature_pre_hash_shake256/Makefile b/proofs/cbmc/sign_signature_pre_hash_shake256/Makefile index ad0a7a16d2..5f26dcdf5d 100644 --- a/proofs/cbmc/sign_signature_pre_hash_shake256/Makefile +++ b/proofs/cbmc/sign_signature_pre_hash_shake256/Makefile @@ -28,7 +28,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = sign_signature_pre_hash_shake256 diff --git a/proofs/cbmc/sign_verify/Makefile b/proofs/cbmc/sign_verify/Makefile index 5c0f72eee6..e2c403026d 100644 --- a/proofs/cbmc/sign_verify/Makefile +++ b/proofs/cbmc/sign_verify/Makefile @@ -27,7 +27,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = sign_verify diff --git a/proofs/cbmc/sign_verify_extmu/Makefile b/proofs/cbmc/sign_verify_extmu/Makefile index f3e8ce694f..33215d0303 100644 --- a/proofs/cbmc/sign_verify_extmu/Makefile +++ b/proofs/cbmc/sign_verify_extmu/Makefile @@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = sign_verify_extmu diff --git a/proofs/cbmc/sign_verify_pre_hash_internal/Makefile b/proofs/cbmc/sign_verify_pre_hash_internal/Makefile index be076c4948..5145b9613b 100644 --- a/proofs/cbmc/sign_verify_pre_hash_internal/Makefile +++ b/proofs/cbmc/sign_verify_pre_hash_internal/Makefile @@ -27,7 +27,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = sign_verify_pre_hash_internal diff --git a/proofs/cbmc/sign_verify_pre_hash_shake256/Makefile b/proofs/cbmc/sign_verify_pre_hash_shake256/Makefile index bd8b24bc14..744c0d258d 100644 --- a/proofs/cbmc/sign_verify_pre_hash_shake256/Makefile +++ b/proofs/cbmc/sign_verify_pre_hash_shake256/Makefile @@ -28,7 +28,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = sign_verify_pre_hash_shake256 diff --git a/proofs/cbmc/sk_s1hat_get_poly/Makefile b/proofs/cbmc/sk_s1hat_get_poly/Makefile index e5f07a2c97..bf318e45af 100644 --- a/proofs/cbmc/sk_s1hat_get_poly/Makefile +++ b/proofs/cbmc/sk_s1hat_get_poly/Makefile @@ -30,7 +30,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = sk_s1hat_get_poly diff --git a/proofs/cbmc/sk_s2hat_get_poly/Makefile b/proofs/cbmc/sk_s2hat_get_poly/Makefile index 1045e1c7ba..3c2c794a85 100644 --- a/proofs/cbmc/sk_s2hat_get_poly/Makefile +++ b/proofs/cbmc/sk_s2hat_get_poly/Makefile @@ -30,7 +30,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = sk_s2hat_get_poly diff --git a/proofs/cbmc/sk_t0hat_get_poly/Makefile b/proofs/cbmc/sk_t0hat_get_poly/Makefile index 8479df1c4e..0dc7bea94c 100644 --- a/proofs/cbmc/sk_t0hat_get_poly/Makefile +++ b/proofs/cbmc/sk_t0hat_get_poly/Makefile @@ -30,7 +30,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = sk_t0hat_get_poly diff --git a/proofs/cbmc/sys_check_capability/Makefile b/proofs/cbmc/sys_check_capability/Makefile index b4e948b5e2..b177078181 100644 --- a/proofs/cbmc/sys_check_capability/Makefile +++ b/proofs/cbmc/sys_check_capability/Makefile @@ -27,7 +27,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:cvc5_arrays_exp CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = is_native_capable diff --git a/proofs/cbmc/unpack_pk_t1/Makefile b/proofs/cbmc/unpack_pk_t1/Makefile index 3ad7617f47..07ca9c820f 100644 --- a/proofs/cbmc/unpack_pk_t1/Makefile +++ b/proofs/cbmc/unpack_pk_t1/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = unpack_pk_t1 diff --git a/proofs/cbmc/use_hint/Makefile b/proofs/cbmc/use_hint/Makefile index 951f40124a..5adc11b7c3 100644 --- a/proofs/cbmc/use_hint/Makefile +++ b/proofs/cbmc/use_hint/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = use_hint diff --git a/proofs/cbmc/value_barrier_i64/Makefile b/proofs/cbmc/value_barrier_i64/Makefile index b985677d6d..38243e62c2 100644 --- a/proofs/cbmc/value_barrier_i64/Makefile +++ b/proofs/cbmc/value_barrier_i64/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = mld_value_barrier_i64 diff --git a/proofs/cbmc/value_barrier_u32/Makefile b/proofs/cbmc/value_barrier_u32/Makefile index eb0f557a90..00e4c1e96d 100644 --- a/proofs/cbmc/value_barrier_u32/Makefile +++ b/proofs/cbmc/value_barrier_u32/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = mld_value_barrier_u32 diff --git a/proofs/cbmc/value_barrier_u8/Makefile b/proofs/cbmc/value_barrier_u8/Makefile index 9639b97afc..86c17f07a3 100644 --- a/proofs/cbmc/value_barrier_u8/Makefile +++ b/proofs/cbmc/value_barrier_u8/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:cvc5_arrays_exp CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = mld_value_barrier_u8 diff --git a/proofs/cbmc/yvec_get_poly/Makefile b/proofs/cbmc/yvec_get_poly/Makefile index 02fc1dbcdc..953453d7e0 100644 --- a/proofs/cbmc/yvec_get_poly/Makefile +++ b/proofs/cbmc/yvec_get_poly/Makefile @@ -29,7 +29,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = yvec_get_poly diff --git a/proofs/cbmc/yvec_init/Makefile b/proofs/cbmc/yvec_init/Makefile index c2c81da4de..ae8bc32357 100644 --- a/proofs/cbmc/yvec_init/Makefile +++ b/proofs/cbmc/yvec_init/Makefile @@ -29,7 +29,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:bitwuzla CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = yvec_init