Automated Reasoning with Nested Datatypes

Tomer Hakak, Yoni Zohar, Andrew Reynolds +2

We introduce a theory of nested datatypes. The theory is obtained by restricting the naive combination of datatypes and arrays, so as to prevent non-standard models from emerging.…