Skip to content

Commit 4435c12

Browse files
committed
Add --no-standard-checks to regression/cbmc-incr-smt2 runner scripts
1 parent 457b953 commit 4435c12

File tree

2 files changed

+4
-4
lines changed

2 files changed

+4
-4
lines changed
Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,13 @@
11
add_test_pl_profile(
22
"cbmc-incr-smt2-z3"
3-
"$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation"
3+
"$<TARGET_FILE:cbmc> --no-standard-checks --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation"
44
"-C;-s;new-smt-z3"
55
"CORE"
66
)
77

88
add_test_pl_profile(
99
"cbmc-incr-smt2-cvc5"
10-
"$<TARGET_FILE:cbmc> --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --validate-goto-model --validate-ssa-equation"
10+
"$<TARGET_FILE:cbmc> --no-standard-checks --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --validate-goto-model --validate-ssa-equation"
1111
"-C;-s;new-smt-cvc5"
1212
"CORE"
1313
)

regression/cbmc-incr-smt2/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,10 @@ include ../../src/common
66
test: test.z3 test.cvc5
77

88
test.z3:
9-
@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation"
9+
@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation"
1010

1111
test.cvc5:
12-
@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --validate-goto-model --validate-ssa-equation"
12+
@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --validate-goto-model --validate-ssa-equation"
1313

1414
tests.log: ../test.pl test
1515

0 commit comments

Comments
 (0)