blob: fbf8e4e3daeedf32efa92586f0c502cd37e113bc (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
//Translation from addsub_double_exact.c
//Should Verify
procedure main() returns () {
var x : float(11 53);
var y : float(11 53);
var z : float(11 53);
var r : float(11 53);
x := fp(10000000 11 53);
y := x + fp(1 11 53);
z := x - fp(1 11 53);
r := y - z;
assert r == fp(2 11 53);
}
|