Skip to content

Fix the extraction of finite maps from Z3

Viktor Kuncak requested to merge github/fork/brunnerant/improve-smtlib-map-extraction into master

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.

Merge request reports