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