H. Smith
-
2010-08-12
Menu
▾
▴
#24 Old-style intermediate variables when using existentials
When an ensures clause contains "there exists", VCs get generated using the old-style (e.g., "?S") intermediate variables in some places instead of the new-style (e.g., "S'"). This is especially confusing since the same logical variable may be referred to in both different ways inside the same VC. You should be able to reproduce the bug with the realization included in the tarball attached.