Skip to content

Commit

Permalink
Keep ghost vars when checking realizability of a node's environment
Browse files Browse the repository at this point in the history
  • Loading branch information
daniel-larraz committed Dec 11, 2024
1 parent f783c33 commit dc7da94
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion src/lustre/lustreGenRefTypeImpNodes.ml
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,8 @@ let node_decl_to_contracts
= fun pos ctx (id, extern, _, params, inputs, outputs, locals, _, contract) ->
let base_contract = match contract with | None -> [] | Some (_, contract) -> contract in
let contract' = List.filter_map (fun ci ->
match ci with
match ci with
| A.GhostConst _ | GhostVars _ -> Some ci
| A.Assume (pos, name, b, expr) -> Some (A.Guarantee (pos, name, b, expr))
| _ -> None
) base_contract in
Expand Down

0 comments on commit dc7da94

Please sign in to comment.