diff --git a/regression/contracts-dfcc/quantifiers-loops-fresh-bound-vars-smt/test.desc b/regression/contracts-dfcc/quantifiers-loops-fresh-bound-vars-smt/test.desc
index 540f1b7402b..1fafe2e32fc 100644
--- a/regression/contracts-dfcc/quantifiers-loops-fresh-bound-vars-smt/test.desc
+++ b/regression/contracts-dfcc/quantifiers-loops-fresh-bound-vars-smt/test.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 _ --z3 --slice-formula --no-standard-checks
 ^EXIT=0$
@@ -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.
+