Improve proof speed of invntt_layer()

For this proof we tell CBMC to remove constraints that are not in the cone of influcence of the proof obligations using the "--slice-formula" option. Experiment shows this reduces proof time for this subprogram from about 40s to about 12s on a developer's laptop. Signed-off-by: Rod Chapman <[email protected]>
pq-code-package · Nov 15, 2024 · 12f9b68 · 12f9b68
1 parent 7b5a9e4
commit 12f9b68
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/cbmc/proofs/invntt_layer/Makefile b/cbmc/proofs/invntt_layer/Makefile
@@ -27,6 +27,11 @@ USE_DYNAMIC_FRAMES=1
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--smt2
 
+# For this proof we tell CBMC to remove constraints that are not in the cone of
+# influcence of the proof obligations. Experiment shows this reduces proof
+# time for this subprogram from about 40s to about 12s on a developer's laptop.
+CBMCFLAGS += --slice-formula
+
 FUNCTION_NAME = invntt_layer
 
 # If this proof is found to consume huge amounts of RAM, you can set the