1 files changed, 52 insertions, 0 deletions
diff --git a/Test/test20/TypeSynonyms2.bpl.print.expect b/Test/test20/TypeSynonyms2.bpl.print.expect
new file mode 100644
index 00000000..72b889d9
--- /dev/null
+++ b/Test/test20/TypeSynonyms2.bpl.print.expect
@@ -0,0 +1,52 @@
+
+type Set a = [a]bool;
+
+function union<a>(x: Set a, y: Set a) : Set a;
+
+axiom (forall<a> x: Set a, y: Set a, z: a :: (x[z] || y[z]) == union(x, y)[z]);
+
+const intSet0: Set int;
+
+axiom (forall x: int :: intSet0[x] == (x == 0 || x == 2 || x == 3));
+
+const intSet1: Set int;
+
+axiom (forall x: int :: intSet1[x] == (x == -5 || x == 3));
+
+procedure P();
+
+
+
+implementation P()
+{
+    assert (forall x: int :: union(intSet0, intSet1)[x] == (x == -5 || x == 0 || x == 2 || x == 3));
+}
+
+
+
+type Set a = [a]bool;
+
+function union<a>(x: Set a, y: Set a) : Set a;
+
+axiom (forall<a> x: Set a, y: Set a, z: a :: x[z] || y[z] <==> union(x, y)[z]);
+
+const intSet0: Set int;
+
+axiom (forall x: int :: intSet0[x] <==> x == 0 || x == 2 || x == 3);
+
+const intSet1: Set int;
+
+axiom (forall x: int :: intSet1[x] <==> x == -5 || x == 3);
+
+procedure P();
+
+
+
+implementation P()
+{
+    assert (forall x: int :: union(intSet0, intSet1)[x] <==> x == -5 || x == 0 || x == 2 || x == 3);
+}
+
+
+
+Boogie program verifier finished with 0 verified, 0 errors