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