Skip to content

Commit d376e43

Browse files
committed
CBMC: pack_pk increase CBMC_OBJECT_BITS 8 -> 11
Signed-off-by: Matthias J. Kannwischer <[email protected]>
1 parent 705e6d9 commit d376e43

File tree

1 file changed

+1
-2
lines changed

1 file changed

+1
-2
lines changed

proofs/cbmc/pack_pk/Makefile

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,6 @@ USE_DYNAMIC_FRAMES=1
2626
# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
2727
EXTERNAL_SAT_SOLVER=
2828
CBMCFLAGS=--smt2
29-
CBMCFLAGS += --slice-formula
3029

3130
FUNCTION_NAME = pack_pk
3231

@@ -37,7 +36,7 @@ FUNCTION_NAME = pack_pk
3736
# EXPENSIVE = true
3837

3938
# This function is large enough to need...
40-
CBMC_OBJECT_BITS = 8
39+
CBMC_OBJECT_BITS = 11
4140

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

0 commit comments

Comments
 (0)