const x: int;

const y: int;

const z: int;

const r: real;

const s: real;

const t: real;

const P: bool;

const Q: bool;

const R: bool;

axiom x * (y + z) == x + y * z;

axiom x * y + z == (x + y) * z;

axiom x * y * z == x * y * z;

axiom x * y * z * x == x * y * z;

axiom x div y div z == x div (y div z);

axiom x div y div (z div x) == x div y div z;

axiom x + y mod z == y mod z + x;

axiom (x + y) mod z == x mod z + y mod z;

axiom x / y / z == x / (y / z);

axiom x / y / (z / x) == x / y / z;

axiom x / s / z == x / (s / z);

axiom x / s / (z / x) == x / s / z;

axiom r / s / t == r / (s / t);

axiom r / s / (t / r) == r / s / t;

axiom r * s / t == r * s / t;

axiom r / s * t == r / s * t;

axiom (r * s) ** t == r ** t * s ** t;

axiom r ** (s + t) == r ** s * r ** t;

axiom int(real(x)) == x;

axiom r >= 0e0 ==> real(int(r)) <= r;

axiom int(0e0 - 2e-2) == 0;

axiom int(0e0 - 35e0) == -35;

axiom int(27e-1) == 2;

axiom x - y - z == x - (y - z);

axiom x - y - (z - x) == x - y - z;

axiom x + y - z - x + y == 0;

axiom x + y - z - x + y == x + y - (z - (x + y));

axiom P ==> Q ==> R <==> P ==> Q ==> R;

axiom (P ==> Q) ==> R ==> P <==> (P ==> Q) ==> R;

axiom P <==> Q <==> R;

axiom P ==> Q <==> Q ==> R <==> R ==> P;

axiom (P && Q) || (Q && R);

axiom (P || Q) && (Q || R);

axiom P || Q || Q || R;

axiom P && Q && Q && R;

function f(int) : int;

axiom (forall x: int :: {:xname "hello"} {:weight 5} {:ValueFunc f(x + 1)} { f(x + x) } { f(x) * f(x) } {:nopats f(x + x + x) } f(f(x)) < 200);

Boogie program verifier finished with 0 verified, 0 errors