From 79dabec536e5022d9bffb1918613f928b92c4323 Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Wed, 13 Nov 2024 12:47:13 +0000 Subject: [PATCH] CBMC: Increase OBJECT_BITS in poly_invntt_tomont proof We see spurious failures of poly_invntt_tomont, and bumping OBJECT_BITS is an attempt to fix those. It's to be determined whether this is indeed the root cause. Signed-off-by: Hanno Becker --- cbmc/proofs/poly_invntt_tomont/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cbmc/proofs/poly_invntt_tomont/Makefile b/cbmc/proofs/poly_invntt_tomont/Makefile index 110a37f26..211c0f5b9 100644 --- a/cbmc/proofs/poly_invntt_tomont/Makefile +++ b/cbmc/proofs/poly_invntt_tomont/Makefile @@ -36,7 +36,7 @@ FUNCTION_NAME = poly_invntt_tomont # EXPENSIVE = true # This function is large enough to need... -CBMC_OBJECT_BITS = 12 +CBMC_OBJECT_BITS = 13 # If you require access to a file-local ("static") function or object to conduct # your proof, set the following (and do not include the original source file