Closed alexandernutz closed 6 years ago
setting: memloc-array style preprocessing in heap separator (might also apply to freezevar-style)
what we need: an extra subdomain that handles constraints of the form "e in S", where S is a set of elements of some finite/enumeration type
Is implemented and works, as far as I can tell, so I am closing the issue.
setting: memloc-array style preprocessing in heap separator (might also apply to freezevar-style)
what we need: an extra subdomain that handles constraints of the form "e in S", where S is a set of elements of some finite/enumeration type