test/smt/real.unsat.sail


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
28
29
30
31
32
33

default Order dec

$include <prelude.sail>
$include <real.sail>

$property
val prop : (real, real, real) -> bool effect {escape}

function prop(x, y, z) = {
  assert(x * y == y * x);
  assert(x * (y * z) == (x * y) * z);
  assert(x - x == 0.0);
  assert(x * 0.0 == 0.0);
  assert(x * 1.0 == x);

  if not_bool(x == 0.0) then {
    assert(x * (y / x) == y)
  };

  // Comparisons
  assert(x <= x);
  assert(x >= x);
  if x > y then {
    assert(y < x)
  };
  if x < y & y < z then {
    assert(x < z)
  };
  if x <= y & y <= x then {
    assert(x == y)
  };
  true
}