From f7c358520ce9d6be4d6ab013cd5f4458b19bb8e7 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Sat, 16 Nov 2024 10:15:27 -0600 Subject: [PATCH] Do not add proof obligation for subrange free constants --- src/lustre/lustreAstNormalizer.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/lustre/lustreAstNormalizer.ml b/src/lustre/lustreAstNormalizer.ml index 6f0abf2c7..aa57e6a7d 100644 --- a/src/lustre/lustreAstNormalizer.ml +++ b/src/lustre/lustreAstNormalizer.ml @@ -1194,19 +1194,19 @@ and normalize_node info map let gids7 = locals |> List.filter (function | A.NodeVarDecl (_, (_, id, _, _)) - | A.NodeConstDecl (_, FreeConst (_, id, _)) | A.NodeConstDecl (_, TypedConst (_, id, _, _)) -> let ty = get_type_of_id info node_id id in Ctx.type_contains_subrange ctx ty || Ctx.type_contains_ref ctx ty + | A.NodeConstDecl (_, FreeConst _) | A.NodeConstDecl (_, UntypedConst _) -> false) |> List.fold_left (fun acc l -> match l with | A.NodeVarDecl (p, (_, id, _, _)) - | A.NodeConstDecl (p, FreeConst (_, id, _)) | A.NodeConstDecl (p, TypedConst (_, id, _, _)) -> let ty = get_type_of_id info node_id id in let ty = AIC.inline_constants_of_lustre_type info.context ty in let gids = union acc (mk_fresh_subrange_constraint Local info p (Some node_id) id ty) in union gids (mk_fresh_refinement_type_constraint Local info p (A.Ident (p, id)) ty) + | A.NodeConstDecl (_, FreeConst _) | A.NodeConstDecl (_, UntypedConst _)-> assert false) (empty ()) in