summaryrefslogtreecommitdiff
path: root/tests/source/test2.scade
diff options
context:
space:
mode:
Diffstat (limited to 'tests/source/test2.scade')
-rw-r--r--tests/source/test2.scade8
1 files changed, 8 insertions, 0 deletions
diff --git a/tests/source/test2.scade b/tests/source/test2.scade
new file mode 100644
index 0000000..28a3e2d
--- /dev/null
+++ b/tests/source/test2.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 = if i < 0 then 42 else 12;
+ b = 0;
+ c = 0;
+tel