d5397effc2
- Move execstack fixing to spec file from patch
- Moved patch descriptions to initial patch declaration as in examples in
Fedora documentation
- New Caduceus, Krakatoa documentation
- Update test result from small test min.mlw
- Added CVC3 interfacing capabilities
- Removed patch for gwhy configuration, as there is a new mechanism for
this
45 lines
789 B
Text
45 lines
789 B
Text
logic eq_unit : unit, unit -> prop
|
|
|
|
logic neq_unit : unit, unit -> prop
|
|
|
|
logic eq_bool : bool, bool -> prop
|
|
|
|
logic neq_bool : bool, bool -> prop
|
|
|
|
logic lt_int : int, int -> prop
|
|
|
|
logic le_int : int, int -> prop
|
|
|
|
logic gt_int : int, int -> prop
|
|
|
|
logic ge_int : int, int -> prop
|
|
|
|
logic eq_int : int, int -> prop
|
|
|
|
logic neq_int : int, int -> prop
|
|
|
|
logic add_int : int, int -> int
|
|
|
|
logic sub_int : int, int -> int
|
|
|
|
logic mul_int : int, int -> int
|
|
|
|
logic div_int : int, int -> int
|
|
|
|
logic mod_int : int, int -> int
|
|
|
|
logic neg_int : int -> int
|
|
|
|
predicate zwf_zero(a: int, b: int) = ((0 <= b) and (a < b))
|
|
|
|
logic min : int, int -> int
|
|
|
|
axiom min_ax: (forall x:int. (forall y:int. (min(x, y) <= x)))
|
|
|
|
goal f_po_1:
|
|
forall n:int.
|
|
forall r0:int.
|
|
forall r:int.
|
|
(r = min(r0, n)) ->
|
|
(r <= r0)
|
|
|