From ea9ede39e8b8ac06b6b17958decaa96e6705d64b Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Fri, 17 Jan 2025 10:10:36 -0500 Subject: [PATCH] Use simple invalid pointer model with bitwuzla too --- .../quantifiers-loops-fresh-bound-vars-smt/test_bitwuzla.desc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/regression/contracts-dfcc/quantifiers-loops-fresh-bound-vars-smt/test_bitwuzla.desc b/regression/contracts-dfcc/quantifiers-loops-fresh-bound-vars-smt/test_bitwuzla.desc index a79bb9eabb9..6ff51da44b4 100644 --- a/regression/contracts-dfcc/quantifiers-loops-fresh-bound-vars-smt/test_bitwuzla.desc +++ b/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 _ --bitwuzla --slice-formula --no-standard-checks +--dfcc main --apply-loop-contracts --enforce-contract foo --malloc-may-fail --malloc-fail-null --dfcc-simple-invalid-pointer-model _ --bitwuzla --slice-formula --no-standard-checks ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$