CristalCaveGem » LustreC

	  let args = mkexpr loc (Expr_tuple [call_orig; call_inlined]) in 

	  mkexpr loc (Expr_appl ("=", args, None))

      }];

    node_spec = Some 

      {requires = []; 

       ensures = [EnsuresExpr (mkeexpr loc (EExpr_ident ok_ident))];