From 777a9624c46f37ef000201eb0f1bdc0355079e49 Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Fri, 15 Nov 2024 12:29:30 +0000 Subject: [PATCH] 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 --- cbmc/proofs/invntt_layer/Makefile | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/cbmc/proofs/invntt_layer/Makefile b/cbmc/proofs/invntt_layer/Makefile index a2f44bf14..f428d0ff3 100644 --- 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