diff options
Diffstat (limited to 'Test/test20/Coercions.bpl')
| -rw-r--r-- | Test/test20/Coercions.bpl | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/Test/test20/Coercions.bpl b/Test/test20/Coercions.bpl new file mode 100644 index 00000000..cab68149 --- /dev/null +++ b/Test/test20/Coercions.bpl @@ -0,0 +1,17 @@ +
+
+type C, D, E _;
+
+const x:int;
+const c:C;
+const d:D;
+
+axiom (x:int > 0);
+axiom (x:int < 0);
+axiom (x:E <a>[a]int < 0); // impossible coercion
+
+axiom (c:D == d); // impossible coercion
+
+axiom (15:D == d); // impossible coercion
+axiom (15:E int == d); // impossible coercion
+axiom ((18*15):int == 0);
|