When translating a literal map, we generate a ExplicitMap of which elems is a sequence of Maplet. If that is pretty-printed, I get something like:
not := Map(Map(true := false), Map(false := true))
Since we do generate silver nodes directly it could be that we are missing a desugaring step, but it at least seems as though ExplicitMap.desugared is only used to generate smt / boogie.
When translating a literal map, we generate a
ExplicitMapof whichelemsis a sequence ofMaplet. If that is pretty-printed, I get something like:Since we do generate silver nodes directly it could be that we are missing a desugaring step, but it at least seems as though
ExplicitMap.desugaredis only used to generate smt / boogie.