Fix performance regression with z3 via --dfcc-simple-invalid-pointer-model

Author: Remi Delmas

…ers-loops-fresh-bound-vars-smt/test.desc …-fresh-bound-vars-smt/test_bitwuzla.descregression/contracts-dfcc/quantifiers-loops-fresh-bound-vars-smt/test.desc renamed to regression/contracts-dfcc/quantifiers-loops-fresh-bound-vars-smt/test_bitwuzla.desc regression/contracts-dfcc/quantifiers-loops-fresh-bound-vars-smt/test.desc renamed to regression/contracts-dfcc/quantifiers-loops-fresh-bound-vars-smt/test_bitwuzla.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$

regression/contracts-dfcc/quantifiers-loops-fresh-bound-vars-smt/test_z3.desc

@@ -0,0 +1,17 @@
+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 --dfcc-simple-invalid-pointer-model _ --z3 --slice-formula --no-standard-checks
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Tests support for quantifiers in loop contracts with the SMT backend.
+When quantified loop invariants are used, they are inserted three times
+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.
+When z3 is used, for performance we have to activate the simple invalid pointer
+model in the cprover_contracts library.