Skip to content

Commit 540f3b8

Browse files
author
Remi Delmas
committed
Mark regressing test as FUTURE
1 parent f8448a6 commit 540f3b8

File tree

1 file changed

+2
-1
lines changed
  • regression/contracts-dfcc/quantifiers-loops-fresh-bound-vars-smt

1 file changed

+2
-1
lines changed

regression/contracts-dfcc/quantifiers-loops-fresh-bound-vars-smt/test.desc

+2-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE dfcc-only smt-backend broken-cprover-smt-backend
1+
FUTURE dfcc-only smt-backend broken-cprover-smt-backend
22
main.c
33
--dfcc main --apply-loop-contracts --enforce-contract foo --malloc-may-fail --malloc-fail-null _ --z3 --slice-formula --no-standard-checks
44
^EXIT=0$
@@ -13,3 +13,4 @@ in the transformed program (base case assertion, step case assumption,
1313
step case assertion), and each occurrence needs to be rewritten with fresh
1414
symbols for the quantified variables. The SMT solver would with an error
1515
whenever this renaming is not properly done.
16+

0 commit comments

Comments
 (0)