KNOWNBUG test for nondeterministic definition of variable

NuSMV allows ASSIGN var := { ... }, which is errored by the type checker.

Author: kroening

regression/smv/assign/assign_set2.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+assign_set2.smv
+--bdd
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This does not type check.

regression/smv/assign/assign_set2.smv

@@ -0,0 +1,9 @@
+MODULE main
+
+VAR x : 0..6;
+
+-- this is a nondeterministic choice
+ASSIGN x := { 1, 4 };
+
+SPEC AG x != 2
+SPEC EX x = 1