Fix and extend test suite

kind2-mc · Sep 26, 2023 · 2c2ca73 · 2c2ca73
1 parent a49963f
commit 2c2ca73
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 1 deletion.
diff --git a/tests/ounit/lustre/testLustreFrontend.ml b/tests/ounit/lustre/testLustreFrontend.ml
@@ -57,7 +57,7 @@ let _ = run_test_tt_main ("frontend LustreAstInlineConstants error tests" >::: [
     | Error (`LustreAstInlineConstantsError (_, FreeIntIdentifier _)) -> true
     | _ -> false);
   mk_test "test symbolic subrange bound 2" (fun () ->
-    match load_file "./lustreTypeChecker/bad_subrange_bound_2.lus" with
+    match load_file "./lustreTypeChecker/symbolic_subrange_bound_2.lus" with
     | Error (`LustreAstInlineConstantsError (_, FreeIntIdentifier _)) -> true
     | _ -> false);
 ])

diff --git a/tests/regression/success/const_parameters.lus b/tests/regression/success/const_parameters.lus
@@ -0,0 +1,18 @@
+
+node F() returns (x,y:int)
+let
+   x = 1; y = 2;
+tel
+
+node N(x,y:int;const n: int;m:int) returns (z:int);
+let
+  z = if C>0 then y+m else x+n;
+tel
+
+const C, W:int;
+
+node M(t:int) returns (z:int);
+let
+  z=N(F(), if C>0 then (W+3, t+1) else (2*C, C));
+  check z=t+3 or z=2*C+1;
+tel