Skip to content

Commit dc5de10

Browse files
committed
CBMC: Increase the CBMC_OBJECT_BITS of matvec_mul to 12
- During latest change about adding derandomized config guard, the CBMC proof for `matvec_mul` failed due to SMT-solver return unknown, increadse the CBMC_OBJECT_BITS to fixed it. Signed-off-by: willieyz <[email protected]>
1 parent 4743633 commit dc5de10

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

proofs/cbmc/matvec_mul/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@ FUNCTION_NAME = mlk_matvec_mul
4747
# EXPENSIVE = true
4848

4949
# This function is large enough to need...
50-
CBMC_OBJECT_BITS = 10
50+
CBMC_OBJECT_BITS = 12
5151

5252
# If you require access to a file-local ("static") function or object to conduct
5353
# your proof, set the following (and do not include the original source file

0 commit comments

Comments
 (0)