summaryrefslogtreecommitdiff
path: root/Test/floats/test17.bpl
blob: caa1fa7446439be6e2457355f1c8e341028c10da (plain)
1
2
3
4
5
6
7
8
9
10
11
//Translation from nan_double_range_true-unreach-call.c
//Should verify
//Uggghhhh, should I add support for e?

procedure main() returns () {
	var x : float(11 53);
	havoc x;
	if (x >= fp(-100000000000000000000000000 11 53) && x <= fp(100000000000000000000000000 11 53)) {	
		assert(x==x);
	}
}