We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 4fe9202 commit c3916e8Copy full SHA for c3916e8
regression/contracts-dfcc/quantifiers-loops-fresh-bound-vars-smt/test.desc
@@ -1,6 +1,6 @@
1
CORE dfcc-only smt-backend broken-cprover-smt-backend
2
main.c
3
---dfcc main --apply-loop-contracts --enforce-contract foo --malloc-may-fail --malloc-fail-null _ --z3 --slice-formula
+--dfcc main --apply-loop-contracts --enforce-contract foo --malloc-may-fail --malloc-fail-null _ --z3 --slice-formula --no-standard-checks
4
^EXIT=0$
5
^SIGNAL=0$
6
^VERIFICATION SUCCESSFUL$
0 commit comments