Skip to content

Commit

Permalink
Mark regressing test as FUTURE
Browse files Browse the repository at this point in the history
  • Loading branch information
Remi Delmas committed Jan 14, 2025
1 parent f8448a6 commit 540f3b8
Showing 1 changed file with 2 additions and 1 deletion.
Original file line number Diff line number Diff line change
@@ -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 _ --z3 --slice-formula --no-standard-checks
^EXIT=0$
Expand All @@ -13,3 +13,4 @@ in the transformed program (base case assertion, step case assumption,
step case assertion), and each occurrence needs to be rewritten with fresh
symbols for the quantified variables. The SMT solver would with an error
whenever this renaming is not properly done.

0 comments on commit 540f3b8

Please sign in to comment.