Fix bug with last commit

kind2-mc · Sep 13, 2023 · e9c24e3 · e9c24e3
1 parent a1aa151
commit e9c24e3
Showing 1 changed file with 6 additions and 4 deletions.
diff --git a/src/lustre/lustreSyntaxChecks.ml b/src/lustre/lustreSyntaxChecks.ml
@@ -832,10 +832,12 @@ and check_expr ctx f (expr:LustreAst.expr) =
       (check_expr ctx f e1) >> (check_expr ctx f e2) >> (check_expr_list ctx f e3)
     | RestartEvery (_, _, e1, e2)
       -> (check_expr_list ctx f e1) >> (check_expr ctx f e2)
-    | ChooseOp (_, _, e1, None) -> 
-      (check_expr ctx f e1)
-    | ChooseOp (_, _, e1, Some e2) -> 
-      (check_expr ctx f e1) >> (check_expr ctx f e2)
+    | ChooseOp (_, (_, i, ty), e1, None) -> 
+      let extn_ctx = ctx_add_local ctx i (Some ty) in
+      (check_expr extn_ctx f e1)
+    | ChooseOp (_, (_, i, ty), e1, Some e2) -> 
+      let extn_ctx = ctx_add_local ctx i (Some ty) in
+      (check_expr extn_ctx f e1) >> (check_expr extn_ctx f e2)
     | _ -> Ok ()
   in
   expr' >> r