Test/test21/Real.bpl


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

axiom (forall r: real :: r == 0.0 || r / r == 1.0);

procedure P(a: real, b: real) returns () {
  assume a >= b && a != 0.0 && a >= 1.3579;

  assert 2e0 * (a + 3.0) - 0.5 >= b;
  assert 2e0 * (a + 3.0) - 0.5 > b;
  assert b <= 2e0 * (a + 3.0) - 0.5;
  assert b < 2e0 * (a + 3.0) - 0.5;

  assert 1/2 <= 0.65;
  assert a > 100e-2 ==> 1 / a <= a;
  assert a / 2 != a || a == 0.00;
  assert a != 0.0 ==> a / a == 1.0;

  assert int(a) >= 0 ==> real(3) * a > a;
}