Map.!: given key is not an element in the map

[msaaltink]

sawscript> sat abc {{ \x -> x == 0b }}
[16:54:59.889] Sat: [x = 0]

sawscript> sat z3 {{ \x -> x == 0b }}

Map.!: given key is not an element in the map
CallStack (from HasCallStack):
  error, called at libraries/containers/containers/src/Data/Map/Internal.hs:627:17 in containers-0.6.2.1:Data.Map.Internal

[brianhuffman]

Wow, I didn't realize you could write 0b for a 0-bit literal! That's fun!

Anyway, my first thought was that this is similar to #872, because it's specific to values of type [0]. But there's more to it than that. I tried a few variations, and it seems that the error occurs when the body of the sat query simplifies to True.

sawscript> sat z3 {{ \(x:[0]) -> True }}

Map.!: given key is not an element in the map
CallStack (from HasCallStack):
  error, called at libraries/containers/containers/src/Data/Map/Internal.hs:627:17 in containers-0.6.2.1:Data.Map.Internal
sawscript> sat z3 {{ \(x:[0]) -> False }}
[20:35:19.415] Unsat

You can also get a similar error for prove instead of sat, but with True and False reversed.

sawscript> prove z3 {{ \(x:[0]) -> True }}
[20:36:22.685] Valid
sawscript> prove z3 {{ \(x:[0]) -> False }}
[20:36:26.211] prove: 1 unsolved subgoal(s)

Map.!: given key is not an element in the map
CallStack (from HasCallStack):
  error, called at libraries/containers/containers/src/Data/Map/Internal.hs:627:17 in containers-0.6.2.1:Data.Map.Internal

Based on what I've seen, I'd guess that the error arises when we're obtaining a counterexample involving a variable of zero width.