From d0642ee17904f19bafe638a9a529c417b6099482 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Fri, 17 Jan 2025 12:13:16 -0500 Subject: [PATCH] Mark peformance regressing test as KNOWNBUG --- .../quantifiers-loops-fresh-bound-vars-smt/test.desc | 8 +++++++- 1 file changed, 7 insertions(+), 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 index 540f1b7402b..00e429b870d 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 +KNWONBUG 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$ @@ -7,6 +7,12 @@ main.c -- ^warning: ignoring -- + +Marked as KNWONBUG because: +- z3 >v4.12 and up can solve the problem with `--dfcc-simple-invalid-pointer-model`, + but the CI uses older versions; +- bitwuzla >v0.6 can solve the problem but we don't run bitwuzla in CI. + 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,