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

Fixed incorrect variable renaming in bcccc88 #1104

Merged
merged 1 commit into from
Oct 4, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 6 additions & 6 deletions src/lustre/lustreAstNormalizer.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1155,25 +1155,25 @@ and normalize_node info map
in
(* Normalize equations and the contract *)
let nitems, gids8, warnings5 = normalize_list (normalize_item info node_id map) items in
let gids7' = union gids7 gids8 in
let gids8' =
let gids6_8 = union gids6 gids8 in
let gids9 =
if exists_reachability_prop_with_bounds ||
not (StringMap.is_empty gids7'.history_vars) then (
not (StringMap.is_empty gids6_8.history_vars) then (
add_step_counter info
)
else
empty ()
in
let gids9 =
let gids10 =
StringMap.fold
(fun id h_id acc ->
union acc (add_history_var_and_equation info id h_id)
)
gids7'.history_vars
gids6_8.history_vars
(empty ())
in
let new_gids = union_list [union_list gids1; union_list gids2; union_list gids3;
gids4; gids5; gids6; gids7'; gids8'; gids9] in
gids4; gids5; gids7; gids6_8; gids9; gids10] in
let old_gids, warnings6 = normalize_gid_equations info map node_id in
let map = StringMap.add node_id (union old_gids new_gids) map in
(node_id, is_extern, params, inputs, outputs, locals, List.flatten nitems, ncontracts),
Expand Down
8 changes: 8 additions & 0 deletions tests/regression/success/history1.lus
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@

node N(x: int) returns (y: int);
(*@contract
guarantee "G1" exists (z: history(x)) y = z + 1;
*)
let
y = x + 1 -> if any bool then x + 1 else pre y;
tel