We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 62c65f3 commit dfa43d2Copy full SHA for dfa43d2
proofs/cbmc/pack_pk/Makefile
@@ -26,7 +26,6 @@ USE_DYNAMIC_FRAMES=1
26
# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
27
EXTERNAL_SAT_SOLVER=
28
CBMCFLAGS=--smt2
29
-CBMCFLAGS += --slice-formula
30
31
FUNCTION_NAME = pack_pk
32
@@ -37,7 +36,7 @@ FUNCTION_NAME = pack_pk
37
36
# EXPENSIVE = true
38
39
# This function is large enough to need...
40
-CBMC_OBJECT_BITS = 8
+CBMC_OBJECT_BITS = 11
41
42
# If you require access to a file-local ("static") function or object to conduct
43
# your proof, set the following (and do not include the original source file
0 commit comments