fn int_max(n: &str) -> boolExpand description
Comparison / absolute-value / negation / saturating & unchecked arithmetic
operations. Each is modelled with a precise expression over its operands
(see the eff_return_* builders) so non-zero-ness is discharged
conditionally — only when the operands are actually non-zero.