Test/floats/float3.bpl


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27

// RUN: %boogie -proverWarnings:1 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
procedure main() returns () {
	var x : float24e8;
	var y : float24e8;
	var z : float24e8;
	
	z := x + y;
	z := x - y;
	z := x * y;
	assume(y != 0e0f24e8);
	z := x / y;
	
	z := (0e127f24e8 + 0e127f24e8 + 0e0f24e8);
	assert(z == 0e128f24e8);
	
	z := 0e128f24e8 - 0e127f24e8;
	assert(z == 0e127f24e8);
	
	z := 0e127f24e8 * 0e127f24e8;
	assert(z == 0e127f24e8);
	
	z := 0e127f24e8 / 0e127f24e8;
	assert(z == 0e127f24e8);
	
	return;
}