Merge pull request #1532 from diffblue/smv_in1

tautschnig · web-flow · commit b2eb2be1347d · 2025-12-28T21:59:15.000+01:00
KNOWNBUG test for SMV `in` with set on LHS
diff --git a/regression/smv/expressions/smv_in1.desc b/regression/smv/expressions/smv_in1.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+smv_in1.smv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This does not type check.
diff --git a/regression/smv/expressions/smv_in1.smv b/regression/smv/expressions/smv_in1.smv
@@ -0,0 +1,5 @@
+MODULE main
+
+-- "in" allows sets on the lhs
+SPEC { 1, 2 } in { 1, 2, 3 }
+SPEC !({ 1, 2, 4 } in { 1, 2, 3 })
