An index out of range error when combining oneOf and setOfMaps

[ivan-gavran]

Consider the following simple model:

module problem{
    var x: str -> (str -> int)
    val X = Set("A", "B")
    val Y = Set("C", "D")
    val Z = Set(1,2)
    val allPossibleVals = setOfMaps(X, setOfMaps(Y, Z))

    action init =                 
        nondet initVal = allPossibleVals.oneOf()
        x' = initVal

    action step = 
        x' = x

    }   

When running the simulator quint run --max-samples=1 --max-steps=1 problem.qnt, a runtime error occurs:

error: [QNT501] Index out of bounds
[lineNumber]: nondet initVal = allPossibleVals.oneOf()

---

There are two curious things here:

1. If we modify Y to be a singleton set, the problem disappears. (Making X or Z singleton has no effect.)
2. If the set allPossibleVals is evaluated first (in the REPL) and the provided as a constant to the model, the problem disappears.
   Concretely:

module problem{
    var x: str -> (str -> int)
    val allPossibleVals = Set(
        Map("A" -> Map("C" -> 1, "D" -> 1), "B" -> Map("C" -> 1, "D" -> 1)),
        Map("A" -> Map("C" -> 2, "D" -> 1), "B" -> Map("C" -> 1, "D" -> 1)),
        Map("A" -> Map("C" -> 1, "D" -> 2), "B" -> Map("C" -> 1, "D" -> 1)),
        Map("A" -> Map("C" -> 2, "D" -> 2), "B" -> Map("C" -> 1, "D" -> 1)),
        Map("A" -> Map("C" -> 1, "D" -> 1), "B" -> Map("C" -> 2, "D" -> 1)),
        Map("A" -> Map("C" -> 2, "D" -> 1), "B" -> Map("C" -> 2, "D" -> 1)),
        Map("A" -> Map("C" -> 1, "D" -> 2), "B" -> Map("C" -> 2, "D" -> 1)),
        Map("A" -> Map("C" -> 2, "D" -> 2), "B" -> Map("C" -> 2, "D" -> 1)),
        Map("A" -> Map("C" -> 1, "D" -> 1), "B" -> Map("C" -> 1, "D" -> 2)),
        Map("A" -> Map("C" -> 2, "D" -> 1), "B" -> Map("C" -> 1, "D" -> 2)),
        Map("A" -> Map("C" -> 1, "D" -> 2), "B" -> Map("C" -> 1, "D" -> 2)),
        Map("A" -> Map("C" -> 2, "D" -> 2), "B" -> Map("C" -> 1, "D" -> 2)),
        Map("A" -> Map("C" -> 1, "D" -> 1), "B" -> Map("C" -> 2, "D" -> 2)),
        Map("A" -> Map("C" -> 2, "D" -> 1), "B" -> Map("C" -> 2, "D" -> 2)),
        Map("A" -> Map("C" -> 1, "D" -> 2), "B" -> Map("C" -> 2, "D" -> 2)),
        Map("A" -> Map("C" -> 2, "D" -> 2), "B" -> Map("C" -> 2, "D" -> 2))
    )

    action init = 
        nondet initVal = allPossibleVals.oneOf()
        x' = initVal

    action step = 
        x' = x

    }