Skip to content

CBMC: Use a second solver for 149/215 proofs #1423

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hanno-becker merged 1 commit into from
Oct 25, 2026
Merged

CBMC: Use a second solver for 149/215 proofs #1423

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 3 additions & 1 deletion proofs/cbmc/H/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/caddq/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/check_pct/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/ct_cmask_neg_i32/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/ct_cmask_nonzero_u32/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/ct_cmask_nonzero_u8/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/ct_get_optblocker_i64/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/ct_get_optblocker_u32/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/ct_get_optblocker_u8/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/ct_memcmp/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/ct_sel_int32/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/decompose/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/fqmul/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/fqscale/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/intt_native_aarch64/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/intt_native_x86_64/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/keccak_absorb/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/keccak_absorb_once_x4/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/keccak_f1600_x1_native_aarch64/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/keccak_f1600_x1_native_aarch64_v84a/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/keccak_f1600_x4_native_aarch64_v84a/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/keccak_f1600_x4_native_avx2/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/keccak_finalize/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/keccak_init/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/keccak_squeeze/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/keccak_squeezeblocks_x4/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/keccakf1600_extract_bytes/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/keccakf1600_extract_bytes_BE/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/keccakf1600_permute/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/keccakf1600_permute_c/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/keccakf1600_permute_native/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/keccakf1600_xor_bytes/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/keccakf1600_xor_bytes_BE/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/keccakf1600x4_extract_bytes/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading
Loading