Unable to handle identical var names in different CoCoSpec nodes?
Closed this issue · 0 comments
wangte1987 commented
example_naming_issue_PP.KIND2.lus.txt
Hi Daniel,
I am getting this error on the attached example. It happens when there are vars with identical names but in different contract nodes. I have gotten this on an older version of Kind2 that I compiled (v1.1.0-292-gad768f58) as well as the version that I just compiled from the latest developer's branch.
line 73 col. 1: Failure cause: Duplicate definition for Assume_1
line 73 col. 1: Failure cause: unexpected error in treatment of ghost variable Assume_1: LustreAst.Parser_error
Best,
Tim