mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
e6a11b4b11
support for unary -, div and mod in logic support for <-> in logic support for calls inside conditions of if and while support for `check` fixed compilation warnings
11 lines
144 B
Plaintext
11 lines
144 B
Plaintext
use int.Int
|
|
|
|
val ref x : int
|
|
|
|
let f (a : int) : int = a + a
|
|
|
|
let main [@bddinfer] () =
|
|
let temp = f 6 in
|
|
x <- temp;
|
|
assert { x = 12 }
|