From 29cd08a4f0a1baf9410043e021c87eb1b7e3f951 Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Fri, 26 Jun 2026 16:27:11 +0100 Subject: [PATCH] Update prover choice and/or tactic for these long-running proofs These choices appear to favour the SMT encoding of CBMC 6.10.0 Signed-off-by: Rod Chapman --- proofs/cbmc/ct_memcmp/Makefile | 2 +- proofs/cbmc/invntt_layer/Makefile | 2 +- proofs/cbmc/polyvecl_pointwise_acc_montgomery_c/Makefile | 2 +- proofs/cbmc/rej_uniform_native/Makefile | 2 +- proofs/cbmc/rej_uniform_native_aarch64/Makefile | 2 +- 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/proofs/cbmc/ct_memcmp/Makefile b/proofs/cbmc/ct_memcmp/Makefile index 765ba07b5..a9cb59772 100644 --- a/proofs/cbmc/ct_memcmp/Makefile +++ b/proofs/cbmc/ct_memcmp/Makefile @@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--smt2 +CBMCFLAGS=--bitwuzla FUNCTION_NAME = mld_ct_memcmp diff --git a/proofs/cbmc/invntt_layer/Makefile b/proofs/cbmc/invntt_layer/Makefile index b1503d8a5..b864d37d5 100644 --- a/proofs/cbmc/invntt_layer/Makefile +++ b/proofs/cbmc/invntt_layer/Makefile @@ -26,7 +26,7 @@ USE_DYNAMIC_FRAMES=1 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--smt2 +CBMCFLAGS=--bitwuzla FUNCTION_NAME = mld_invntt_layer diff --git a/proofs/cbmc/polyvecl_pointwise_acc_montgomery_c/Makefile b/proofs/cbmc/polyvecl_pointwise_acc_montgomery_c/Makefile index 388f2aa55..cfaab9681 100644 --- a/proofs/cbmc/polyvecl_pointwise_acc_montgomery_c/Makefile +++ b/proofs/cbmc/polyvecl_pointwise_acc_montgomery_c/Makefile @@ -31,7 +31,7 @@ USE_DYNAMIC_FRAMES=1 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--external-smt2-solver $(PROOF_ROOT)/lib/z3_no_bv_extract --z3 +CBMCFLAGS=--smt2 FUNCTION_NAME = mld_polyvecl_pointwise_acc_montgomery_c diff --git a/proofs/cbmc/rej_uniform_native/Makefile b/proofs/cbmc/rej_uniform_native/Makefile index dfa85d68b..18b42ab19 100644 --- a/proofs/cbmc/rej_uniform_native/Makefile +++ b/proofs/cbmc/rej_uniform_native/Makefile @@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--smt2 +CBMCFLAGS=--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 2a95e3ef6..722664f77 100644 --- a/proofs/cbmc/rej_uniform_native_aarch64/Makefile +++ b/proofs/cbmc/rej_uniform_native_aarch64/Makefile @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--smt2 +CBMCFLAGS=--bitwuzla FUNCTION_NAME = rej_uniform_native_aarch64