Mark test that blows up as FUTURE

Remi Delmas · Remi Delmas · commit 86902292e642 · 2025-01-17T10:10:14.000-05:00
diff --git a/regression/contracts-dfcc/quantifiers-loops-fresh-bound-vars-smt/test_z3.desc b/regression/contracts-dfcc/quantifiers-loops-fresh-bound-vars-smt/test_z3.desc
@@ -1,4 +1,4 @@
-CORE dfcc-only smt-backend broken-cprover-smt-backend
+FUTURE dfcc-only smt-backend broken-cprover-smt-backend
 main.c
 --dfcc main --apply-loop-contracts --enforce-contract foo --malloc-may-fail --malloc-fail-null --dfcc-simple-invalid-pointer-model _ --z3 --slice-formula --no-standard-checks
 ^EXIT=0$

Original file line number	Diff line number	Diff 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`
`2`	`2`	`main.c`
`3`	`3`	`--dfcc main --apply-loop-contracts --enforce-contract foo --malloc-may-fail --malloc-fail-null --dfcc-simple-invalid-pointer-model _ --z3 --slice-formula --no-standard-checks`
`4`	`4`	`^EXIT=0$`