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 <[email protected]>
pq-code-package · Nov 13, 2024 · 79dabec · 79dabec
1 parent a9dcce6
commit 79dabec
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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