Skip to content

CBMC: Add more cvc5 proofs #1491

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 2 commits into from
Oct 25, 2026
Merged

CBMC: Add more cvc5 proofs #1491

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
15fe7d6
CBMC: Use a second solver for 149/215 proofs
mkannwischer Sep 9, 2026
721f3e7
CBMC: Add cvc5 profiles with quantifier instantiation
mkannwischer Oct 24, 2026
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
12 changes: 11 additions & 1 deletion proofs/cbmc/Makefile.common
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -191,7 +191,7 @@ CBMC_DM_ILP32_CBMC_FLAG := --ILP32
CBMC_DM_ILP32_INCLUDE := $(CBMC_ROOT)/cbmc/include/ILP32

# Solver profile IDs name the executable and all solver-specific options.
CBMC_SOLVER_PROFILES_ALL := z3 z3_smt_only z3_no_bv_extract bitwuzla cvc5_arrays_exp
CBMC_SOLVER_PROFILES_ALL := z3 z3_smt_only z3_no_bv_extract bitwuzla cvc5_arrays_exp cvc5_mbqi_enum cvc5_enum_inst

CBMC_PROFILE_z3_BACKEND := --smt2
CBMC_PROFILE_z3_PROVER_NAME := Z3
Expand Down Expand Up @@ -220,6 +220,16 @@ CBMC_PROFILE_cvc5_arrays_exp_PROVER_NAME := cvc5
CBMC_PROFILE_cvc5_arrays_exp_SMT_FORMAT := --cvc5
CBMC_PROFILE_cvc5_arrays_exp_FLAGS := --external-smt2-solver $(PROOF_ROOT)/lib/cvc5_arrays_exp --cvc5

CBMC_PROFILE_cvc5_mbqi_enum_BACKEND := --cvc5
CBMC_PROFILE_cvc5_mbqi_enum_PROVER_NAME := cvc5
CBMC_PROFILE_cvc5_mbqi_enum_SMT_FORMAT := --cvc5
CBMC_PROFILE_cvc5_mbqi_enum_FLAGS := --external-smt2-solver $(PROOF_ROOT)/lib/cvc5_mbqi_enum --cvc5

CBMC_PROFILE_cvc5_enum_inst_BACKEND := --cvc5
CBMC_PROFILE_cvc5_enum_inst_PROVER_NAME := cvc5
CBMC_PROFILE_cvc5_enum_inst_SMT_FORMAT := --cvc5
CBMC_PROFILE_cvc5_enum_inst_FLAGS := --external-smt2-solver $(PROOF_ROOT)/lib/cvc5_enum_inst --cvc5

# Make evaluates the configuration checks below before running target recipes.
# The runner queries these metadata targets before selecting CBMC_DM/CBMC_SOLVER.
CBMC_INTROSPECTION_TARGETS := echo-supported-configs echo-default-config echo-solver-profiles echo-data-models echo-proof-uid echo-project-name litani-path
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
5 changes: 4 additions & 1 deletion proofs/cbmc/intt_native_rv32im_fastmul/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,10 @@ USE_FUNCTION_CONTRACTS = mld_intt_rv32im_fastmul_asm
APPLY_LOOP_CONTRACTS = on
USE_DYNAMIC_FRAMES = 1

CBMC_SUPPORTED_CONFIGS = ILP32:z3 LP64:z3
CBMC_SUPPORTED_CONFIGS = \
ILP32:z3 \
LP64:z3 \
LP64:cvc5_mbqi_enum
CBMC_DEFAULT_CONFIG = ILP32:z3
CBMC_OBJECT_BITS = 8

Expand Down
5 changes: 4 additions & 1 deletion proofs/cbmc/intt_native_rv32im_slowmul/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,10 @@ USE_FUNCTION_CONTRACTS = mld_intt_rv32im_slowmul_asm
APPLY_LOOP_CONTRACTS = on
USE_DYNAMIC_FRAMES = 1

CBMC_SUPPORTED_CONFIGS = ILP32:z3 LP64:z3
CBMC_SUPPORTED_CONFIGS = \
ILP32:z3 \
LP64:z3 \
LP64:cvc5_mbqi_enum
CBMC_DEFAULT_CONFIG = ILP32:z3
CBMC_OBJECT_BITS = 8

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
Loading
Loading