Fix the extraction of finite maps from Z3
Created by: brunnerant
This PR fixes a special case where finite maps are not correctly extracted. This happens for the special case where the value type of the map is BooleanType
. Z3 sometimes represents those in that form: (lambda ((x KeyType)) (= x someKey))
. That should be extracted as a finite map where someKey
maps to true
and the rest to false
.
That case is currently not handled and I encountered a case where the output from stainless was misleading because of that extraction problem.