We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 0262ae1 commit 3ce9fceCopy full SHA for 3ce9fce
regression/contracts-dfcc/quantifiers-loops-fresh-bound-vars-smt/test.desc
@@ -1,4 +1,4 @@
1
-KNOWNBUG dfcc-only smt-backend broken-cprover-smt-backend
+FUTURE 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 --no-standard-checks
4
^EXIT=0$
@@ -8,7 +8,7 @@ main.c
8
^warning: ignoring
9
--
10
11
-Marked as KNOWNBUG because:
+Marked as FUTURE because:
12
- z3 >v4.12 and up can solve the problem with `--dfcc-simple-invalid-pointer-model`,
13
but the CI uses older versions;
14
- bitwuzla >v0.6 can solve the problem but we don't run bitwuzla in CI.
0 commit comments