Skip to content

Commit 063e6f8

Browse files
rod-chapmanhanno-becker
authored andcommitted
CBMC: Speed up proof of polyvec_matrix_expand
Signed-off-by: Rod Chapman <rodchap@amazon.com>
1 parent 7a489d3 commit 063e6f8

File tree

1 file changed

+2
-1
lines changed
  • proofs/cbmc/polyvec_matrix_expand

1 file changed

+2
-1
lines changed

proofs/cbmc/polyvec_matrix_expand/Makefile

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,8 @@ USE_DYNAMIC_FRAMES=1
2626

2727
# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
2828
EXTERNAL_SAT_SOLVER=
29-
CBMCFLAGS=--smt2 --arrays-uf-always --slice-formula
29+
CBMCFLAGS=--external-smt2-solver $(PROOF_ROOT)/lib/z3_no_bv_extract --z3
30+
CBMCFLAGS += --slice-formula
3031

3132
FUNCTION_NAME = polyvec_matrix_expand
3233

0 commit comments

Comments
 (0)