Propagate counterexample into Unsafe.bads

[janvrany]

I'd like to see some tests to make sure this keeps working. Perhaps even something like:

commit c52cc672842a0ecdac90658e9e57e9f8a0f2cd55 (HEAD -> merge-propagate-counterexamples)
Author: Jan Vrany <jan.vrany@labware.com>
Date:   Fri May 3 16:08:52 2024 +0100

    Test that every Unsafe contains a counterexample in `bads`

diff --git a/src/SpriteLang-Tests/SpriteLangTest.class.st b/src/SpriteLang-Tests/SpriteLangTest.class.st
index fc318f33..e9d3a13b 100644
--- a/src/SpriteLang-Tests/SpriteLangTest.class.st
+++ b/src/SpriteLang-Tests/SpriteLangTest.class.st
@@ -19,8 +19,13 @@ SpriteLangTest >> proveSafe: source [

 { #category : #running }
 SpriteLangTest >> proveUnsafe: source [
-       | prog |
+       | prog unsafe |
        prog := ΛκParser parse: source.
        self deny: prog isPetitFailure.
-       self deny: prog solve isSafe
+
+       unsafe := prog solve.
+       self deny: unsafe isSafe.
+       unsafe bads do:[:bad |
+               bad value value isKindOf: Z3Model
+       ].
 ]

[shingarov]

I like that diff. Do you want to push it on this branch and see what CI says?

[shingarov]

Of course, do: should become something like allSatisfy:, and then assert:.

[janvrany]

Of course, do: should become something like allSatisfy:, and then assert:. Oh, of course, let me fix that.

[janvrany]

OK, see 6dd949a. With this change. LGTM. If you're happy with it. please merge.