Merge pull request #1058 from lorchrob/subrange-props

Always include subrange properties on output variables as guarantees
kind2-mc · Mar 28, 2024 · 82cb49a · 82cb49a
2 parents abad8d7 + e8ef9e3
commit 82cb49a
Showing 1 changed file with 1 addition and 3 deletions.
diff --git a/src/lustre/lustreNodeGen.ml b/src/lustre/lustreNodeGen.ml
@@ -2077,12 +2077,10 @@ and compile_node_decl gids is_function cstate ctx i ext inputs outputs locals it
       (source, contract_scope, is_original, pos, id, rexpr)
     =
       let sv = H.find !map.state_var (mk_ident id) in
-      let effective_contract = guarantees != [] || modes != [] in
       let constraint_kind = match source with
         | GI.Input -> Some N.Assumption
         | Local -> None
-        | Output -> if not ext && not effective_contract then
-            None else Some N.Guarantee
+        | Output -> Some N.Guarantee
         | Ghost -> Some N.Guarantee
       in
       if is_original then