summaryrefslogtreecommitdiff
path: root/tests/source/test1.scade
diff options
context:
space:
mode:
Diffstat (limited to 'tests/source/test1.scade')
-rw-r--r--tests/source/test1.scade8
1 files changed, 8 insertions, 0 deletions
diff --git a/tests/source/test1.scade b/tests/source/test1.scade
new file mode 100644
index 0000000..f247a57
--- /dev/null
+++ b/tests/source/test1.scade
@@ -0,0 +1,8 @@
+function test(i: int) returns(probe a, b, c: int; exit: bool)
+let
+ assume i_pos : i >= 0;
+ exit = i >= 5;
+ a = i;
+ b = 0;
+ c = 0;
+tel