From 70b1d19a18644142dfb7918319dc0def0092ed7e Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Thu, 14 Nov 2024 21:27:02 +0000 Subject: [PATCH] Add comments to explain the new settings for CBMCFLAGS. The explanatory text is adapted from that appearing in CBMC Issue 8505. Signed-off-by: Rod Chapman --- cbmc/proofs/matvec_mul/Makefile | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/cbmc/proofs/matvec_mul/Makefile b/cbmc/proofs/matvec_mul/Makefile index 24b282a6c..a69aadae3 100644 --- a/cbmc/proofs/matvec_mul/Makefile +++ b/cbmc/proofs/matvec_mul/Makefile @@ -24,7 +24,18 @@ USE_DYNAMIC_FRAMES=1 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--smt2 --no-array-field-sensitivity --arrays-uf-always --slice-formula +CBMCFLAGS=--smt2 + +# For this proof we tell CBMC to +# 1. not decompose arrays into their individual cells +# 2. to model arrays directly as SMT-lib arrays +# 3. to slice constraints that are not in the cone of influcence of the proof obligations +# These options simplify them modelling of arrays and produce much more compact +# SMT files, leaving all array-type reasoning to the SMT solver. +# +# For functions that use large and multi-dimensional arrays, this yields +# a substantial improvement in proof performance. +CBMCFLAGS += --no-array-field-sensitivity --arrays-uf-always --slice-formula FUNCTION_NAME = $(MLKEM_NAMESPACE)matvec_mul