Non-determinism analysis: bug if the involved types are enums nested in structs
Consider an enum type MyEnum = First | Second
and a struct type MyStruct = x : MyEnum
Then the analysis fails with an error message from Z3.
At first sight, the bug is in the translation from AF3 to SMT which
apparently does not deal with the nesting of types.
Therefore this bug could have consequences on any module using SMT.
(from redmine: issue id 1896, created on 2014-01-21, closed on 2014-02-10)