From 61d7e0db472b1093e4a5a3f47f1c5efd765cd255 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Wed, 18 Sep 2024 10:13:03 -0700 Subject: [PATCH] Bogus safety violation checking if a set is a subset of Nat. Part of Github issue $2948 https://github.com/apalache-mc/apalache/issues/2948 --- .unreleased/bug-fixes/BogusSafetyViolationSubsetNat.md | 1 + 1 file changed, 1 insertion(+) create mode 100644 .unreleased/bug-fixes/BogusSafetyViolationSubsetNat.md diff --git a/.unreleased/bug-fixes/BogusSafetyViolationSubsetNat.md b/.unreleased/bug-fixes/BogusSafetyViolationSubsetNat.md new file mode 100644 index 0000000000..5202cdeb18 --- /dev/null +++ b/.unreleased/bug-fixes/BogusSafetyViolationSubsetNat.md @@ -0,0 +1 @@ +Show note that expression is unsupported instead of reporting a counterexample claiming that e.g. `{42} \in SUBSET Nat` is false.