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 3a0e501b536df339d98aac0b3b146eb3f9e2ce3c..f0fd534e3c3dba057d59b22e651fd60705b023fa 100644 (file)
--- 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)