Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Imported node generation bug fix #1085

Merged
merged 1 commit into from
Aug 1, 2024

Conversation

lorchrob
Copy link
Contributor

@lorchrob lorchrob commented Jul 31, 2024

Stop duplicating type declarations when generating imported nodes.

Note: LGI.gen_imp_nodes processes type and constant declarations included in const_inlined_type_and_consts, but these declarations should not be included in the result.

@lorchrob
Copy link
Contributor Author

The bug is exhibited by the following lustre file:

const C: int;
type UserType = subtype { x: int | x < C and x > 0 }; 

node N(x: UserType) returns (y: UserType)
let
    y = x;
tel

when calling with --enable CONTRACTCK

@daniel-larraz daniel-larraz merged commit c69b51e into kind2-mc:develop Aug 1, 2024
4 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants