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..a79bb9eabb9 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,6 +1,6 @@
 CORE 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
+--dfcc main --apply-loop-contracts --enforce-contract foo --malloc-may-fail --malloc-fail-null _ --bitwuzla --slice-formula --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$