Skip to content

CBMC: Add a second solver for 2 slow proofs #1496

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

Draft
mkannwischer wants to merge 2 commits into
base: main
Choose a base branch
from
Draft

CBMC: Add a second solver for 2 slow proofs #1496

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
3554de7
CBMC: Add CaDiCaL SAT profile
mkannwischer Oct 25, 2026
8242234
CBMC: Add a second solver for 2 slow proofs
mkannwischer Oct 25, 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
7 changes: 6 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 cvc5_mbqi_enum cvc5_enum_inst
CBMC_SOLVER_PROFILES_ALL := z3 z3_smt_only z3_no_bv_extract bitwuzla cvc5_arrays_exp cvc5_mbqi_enum cvc5_enum_inst cadical

CBMC_PROFILE_z3_BACKEND := --smt2
CBMC_PROFILE_z3_PROVER_NAME := Z3
Expand Down Expand Up @@ -230,6 +230,11 @@ 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

CBMC_PROFILE_cadical_BACKEND :=
CBMC_PROFILE_cadical_PROVER_NAME := CaDiCaL
CBMC_PROFILE_cadical_SMT_FORMAT :=
CBMC_PROFILE_cadical_FLAGS := --sat-solver cadical

# 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/compute_pack_z/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,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:cadical
CBMC_DEFAULT_CONFIG = LP64:z3_no_bv_extract

FUNCTION_NAME = mld_compute_pack_z
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/pointwise_acc_native_x86_64/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,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:cadical
CBMC_DEFAULT_CONFIG = LP64:z3_smt_only

FUNCTION_NAME = pointwise_acc_native_x86_64
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/poly_decompose_32_native_aarch64/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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:cadical
CBMC_DEFAULT_CONFIG = LP64:z3

FUNCTION_NAME = poly_decompose_32_native_aarch64
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/poly_decompose_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_mbqi_enum
CBMC_DEFAULT_CONFIG = LP64:z3

FUNCTION_NAME = mld_poly_decompose_c
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/poly_decompose_native/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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:cadical
CBMC_DEFAULT_CONFIG = LP64:z3

FUNCTION_NAME = poly_decompose_native
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/poly_decompose_native_x86_64/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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:cadical
CBMC_DEFAULT_CONFIG = LP64:z3

FUNCTION_NAME = poly_decompose_native_x86_64
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/poly_uniform_gamma1/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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:cadical
CBMC_DEFAULT_CONFIG = LP64:z3

FUNCTION_NAME = poly_uniform_gamma1
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/poly_uniform_gamma1_4x/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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:cadical
CBMC_DEFAULT_CONFIG = LP64:z3

FUNCTION_NAME = poly_uniform_gamma1_4x
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/sample_pack_s1_s2/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:cadical
CBMC_DEFAULT_CONFIG = LP64:z3

FUNCTION_NAME = mld_sample_pack_s1_s2
Expand Down
6 changes: 4 additions & 2 deletions proofs/cbmc/sign_keypair_internal/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,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:cadical
CBMC_DEFAULT_CONFIG = LP64:z3_no_bv_extract

FUNCTION_NAME = sign_keypair_internal
Expand All @@ -41,7 +43,7 @@ FUNCTION_NAME = sign_keypair_internal
# EXPENSIVE variable. With new enough versions of the proof tools, this will
# restrict the number of EXPENSIVE CBMC jobs running at once. See the
# documentation in Makefile.common under the "Job Pools" heading for details.
# EXPENSIVE = true
EXPENSIVE = true

# This function is large enough to need...
CBMC_OBJECT_BITS = 12
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/sign_signature_extmu/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:cadical
CBMC_DEFAULT_CONFIG = LP64:z3

FUNCTION_NAME = sign_signature_extmu
Expand Down
4 changes: 3 additions & 1 deletion proofs/cbmc/unpack_sk/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:z3
CBMC_SUPPORTED_CONFIGS = \
LP64:z3 \
LP64:cadical
CBMC_DEFAULT_CONFIG = LP64:z3

FUNCTION_NAME = unpack_sk
Expand Down
Loading