blob: e94ab2c3f02f9b0b6780f50bd2704da0c79834d0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
default Order dec
$include <prelude.sail>
$property
function prop(x: int, y: int(32)) -> bool = {
let add_neg_zero = x + negate(x) == 0;
let add_neg_sub = x + negate(y) == x - y;
let neg_neg = negate(negate(x)) == x;
add_neg_zero & add_neg_sub & neg_neg
}
|
