From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Mon, 21 Dec 2020 19:17:13 +0000 (-0300)
Subject: Have unsat core regression agnostic to number of assertions in core (#5712)
X-Git-Tag: cvc5-1.0.0~2414
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3d65b80f9e19739554ddc4263757d9b98111d14e;p=cvc5.git

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.
---

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)