diff --git a/proofs/cbmc/polyvecl_pointwise_acc_montgomery_c/Makefile b/proofs/cbmc/polyvecl_pointwise_acc_montgomery_c/Makefile
index dd6ca86ce..b9daef4e8 100644
--- a/proofs/cbmc/polyvecl_pointwise_acc_montgomery_c/Makefile
+++ b/proofs/cbmc/polyvecl_pointwise_acc_montgomery_c/Makefile
@@ -39,7 +39,7 @@ FUNCTION_NAME = mld_polyvecl_pointwise_acc_montgomery_c
 # 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