diff options
Diffstat (limited to 'test-suite/output/Sint63Syntax.out')
| -rw-r--r-- | test-suite/output/Sint63Syntax.out | 66 |
1 files changed, 66 insertions, 0 deletions
diff --git a/test-suite/output/Sint63Syntax.out b/test-suite/output/Sint63Syntax.out new file mode 100644 index 0000000000..db14658307 --- /dev/null +++ b/test-suite/output/Sint63Syntax.out @@ -0,0 +1,66 @@ +2%sint63 + : int +2 + : int +-3 + : int +4611686018427387903 + : int +-4611686018427387904 + : int +427 + : int +427 + : int +427 + : int +427 + : int +427 + : int +The command has indeed failed with message: +Cannot interpret this number as a value of type int +The command has indeed failed with message: +Cannot interpret this number as a value of type int +0 + : int +0 + : int +The command has indeed failed with message: +The reference xg was not found in the current environment. +The command has indeed failed with message: +The reference xG was not found in the current environment. +The command has indeed failed with message: +The reference x1 was not found in the current environment. +The command has indeed failed with message: +The reference x was not found in the current environment. +2 + 2 + : int +The command has indeed failed with message: +Cannot interpret this number as a value of type int +The command has indeed failed with message: +Cannot interpret this number as a value of type int +0x1%int63 + : int +0x7fffffffffffffff%int63 + : int +2 + : nat +2%sint63 + : int +t = 2%si63 + : int +t = 2%si63 + : int +2 + : nat +2 + : int +(2 + 2)%sint63 + : int +2 + 2 + : int + = 4 + : int + = 37151199385380486 + : int |