Use bitwuzla when quantifiers are involved

diffblue · Jan 14, 2025 · c22a416 · c22a416
1 parent f487326
commit c22a416
Showing 1 changed file with 1 addition and 1 deletion.
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
@@ -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$