summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
Diffstat (limited to 'tests')
-rw-r--r--tests/source/half.scade2
-rw-r--r--tests/source/updown2.scade2
2 files changed, 2 insertions, 2 deletions
diff --git a/tests/source/half.scade b/tests/source/half.scade
index 541e81c..7e0df60 100644
--- a/tests/source/half.scade
+++ b/tests/source/half.scade
@@ -25,5 +25,5 @@ let
c = a - b;
guarantee c_bounded: c >= 0 and c <= 1;
- guarantee link_c_half: (half and c = 1) or ((not half) and c = 0);
+ guarantee link_c_half: if half then (c = 1) else (c = 0);
tel
diff --git a/tests/source/updown2.scade b/tests/source/updown2.scade
index 29c34ff..72d5bed 100644
--- a/tests/source/updown2.scade
+++ b/tests/source/updown2.scade
@@ -30,7 +30,7 @@ let
guarantee y_bounded: y >= -bound and y <= bound;
z = x + y;
- guarantee x_y_opp: z = 0 and (true -> pre (z = 0));
+ guarantee x_y_opp: z = 0;
tel
node test(i: int) returns(a, b, c: int; exit: bool)