summaryrefslogtreecommitdiff
path: root/Test/test20/Answer
diff options
context:
space:
mode:
Diffstat (limited to 'Test/test20/Answer')
-rw-r--r--Test/test20/Answer8
1 files changed, 4 insertions, 4 deletions
diff --git a/Test/test20/Answer b/Test/test20/Answer
index efa5bced..fa33507e 100644
--- a/Test/test20/Answer
+++ b/Test/test20/Answer
@@ -118,7 +118,7 @@ axiom (forall x: int :: intSet0[x] == (x == 0 || x == 2 || x == 3));
const intSet1: Set int;
-axiom (forall x: int :: intSet1[x] == (x == 0 - 5 || x == 3));
+axiom (forall x: int :: intSet1[x] == (x == -5 || x == 3));
procedure P();
@@ -126,7 +126,7 @@ procedure P();
implementation P()
{
- assert (forall x: int :: union(intSet0, intSet1)[x] == (x == 0 - 5 || x == 0 || x == 2 || x == 3));
+ assert (forall x: int :: union(intSet0, intSet1)[x] == (x == -5 || x == 0 || x == 2 || x == 3));
}
@@ -143,7 +143,7 @@ axiom (forall x: int :: intSet0[x] <==> x == 0 || x == 2 || x == 3);
const intSet1: Set int;
-axiom (forall x: int :: intSet1[x] <==> x == 0 - 5 || x == 3);
+axiom (forall x: int :: intSet1[x] <==> x == -5 || x == 3);
procedure P();
@@ -151,7 +151,7 @@ procedure P();
implementation P()
{
- assert (forall x: int :: union(intSet0, intSet1)[x] <==> x == 0 - 5 || x == 0 || x == 2 || x == 3);
+ assert (forall x: int :: union(intSet0, intSet1)[x] <==> x == -5 || x == 0 || x == 2 || x == 3);
}