Merge pull request kind2-mc#1003 from lorchrob/subrange-bug

Fix bug with subranges
daniel-larraz · Aug 31, 2023 · 7b00f55 · 7b00f55
2 parents 53827fb + 795c64e
commit 7b00f55
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 1 deletion.
diff --git a/src/lustre/lustreTransSys.ml b/src/lustre/lustreTransSys.ml
@@ -489,7 +489,7 @@ let add_constraints_of_type init terms state_var =
 
     (* Get bounds of integer range *)
     let l, u = 
-      (if Type.is_array state_var_type 
+      (if Type.is_int_range state_var_type
       then Type.bounds_of_int_range state_var_type
       else Type.bounds_of_enum state_var_type |> (fun (a, b) -> Some a, Some b))
     in

diff --git a/tests/regression/success/subrange_bug.lus b/tests/regression/success/subrange_bug.lus
@@ -0,0 +1,5 @@
+node main () returns (y: subrange [0, 7] of int); 
+let 
+
+  check y <= 7;
+tel;