mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
20 lines
428 B
Plaintext
20 lines
428 B
Plaintext
|
|
use int.Int
|
|
use mach.float.Double
|
|
|
|
let test (b:int) =
|
|
let x : t = (1.5:t) in
|
|
let y : t = (2.25:t) in
|
|
let z : t = safe_add x y in
|
|
let a : t = safe_mul x z in
|
|
let c : t = (0x1p1023:t) in
|
|
let zer : t = (0.0:t) in
|
|
let _wrong =
|
|
(* wrong tests in parallel to avoid inconsistent context *)
|
|
if b = 0 then safe_div a zer else
|
|
if b = 1 then safe_mul y c else
|
|
if b = 2 then safe_add c c else
|
|
c
|
|
in
|
|
()
|