In single file mode, variables with the same name in `init` and a matching rule don't get unique names but clash
init ^ (s) := new s, ty == T(). [[ e ^ (s) ]] := ty == T().
The twoSubmitted by Hendrik van Antwerpen on 8 September 2016 at 13:43
ty’s get the same unique name in the generated constraints.
For now, fixed it with a work-around that calls init with the project directory even in single file mode.
EDIT: This does cause problems too, because there is no unit for the project in single file mode. And even if there was, the sjaring between files would probably cause problems as well.
Log in to post comments