From 3d65b80f9e19739554ddc4263757d9b98111d14e Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Mon, 21 Dec 2020 16:17:13 -0300 Subject: [PATCH] Have unsat core regression agnostic to number of assertions in core (#5712) Changing our unsat core infrastructure may change the cores we produce. This can be problematic for regressions that hardcode the number of assertions we get (such as this one). This commit changes such a regression to rather expect any core. It is motivated by exactly the previously described issue occurring after using the new proof infrastructure to generate unsat cores, which yielded a smaller core. Kudos to @4tXJ7f for the sed magic. --- test/regress/regress1/issue4335-unsat-core.smt2 | 11 +---------- 1 file changed, 1 insertion(+), 10 deletions(-) diff --git a/test/regress/regress1/issue4335-unsat-core.smt2 b/test/regress/regress1/issue4335-unsat-core.smt2 index 3a0e501b5..f0fd534e3 100644 --- a/test/regress/regress1/issue4335-unsat-core.smt2 +++ b/test/regress/regress1/issue4335-unsat-core.smt2 @@ -1,15 +1,6 @@ -; SCRUBBER: sed -e 's/IP_[0-9]*/IP/' +; SCRUBBER: sed -e '/IP_[0-9]/d' ; EXPECT: unsat ; EXPECT: ( -; EXPECT: IP -; EXPECT: IP -; EXPECT: IP -; EXPECT: IP -; EXPECT: IP -; EXPECT: IP -; EXPECT: IP -; EXPECT: IP -; EXPECT: IP ; EXPECT: ) (set-logic ALL) (set-option :produce-unsat-cores true) -- 2.30.2