Use --arrays-uf-always here to improve proof speed.

rod-chapman · rod-chapman · commit c83ec7ce4a93 · 2025-06-30T10:18:04.000+01:00
Signed-off-by: Rod Chapman &lt;rodchap@amazon.com&gt;
diff --git a/proofs/cbmc/matvec_mul/Makefile b/proofs/cbmc/matvec_mul/Makefile
@@ -35,7 +35,7 @@ CBMCFLAGS=--smt2
 #
 # For functions that use large and multi-dimensional arrays, this yields
 # a substantial improvement in proof performance.
-CBMCFLAGS += --no-array-field-sensitivity
+CBMCFLAGS += --arrays-uf-always
 CBMCFLAGS += --slice-formula
 
 FUNCTION_NAME = mlk_matvec_mul

Original file line number	Diff line number	Diff line change
`@@ -35,7 +35,7 @@ CBMCFLAGS=--smt2`
`35`	`35`	`#`
`36`	`36`	`# For functions that use large and multi-dimensional arrays, this yields`
`37`	`37`	`# a substantial improvement in proof performance.`
`38`		`-CBMCFLAGS += --no-array-field-sensitivity`
	`38`	`+CBMCFLAGS += --arrays-uf-always`
`39`	`39`	`CBMCFLAGS += --slice-formula`
`40`	`40`
`41`	`41`	`FUNCTION_NAME = mlk_matvec_mul`