; Spending-limit decision over mathematical integers, not machine integers.
; Preconditions: 0 <= spent <= limit, amount > 0.
(set-logic QF_LIA)
(declare-const spent Int)
(declare-const amount Int)
(declare-const limit Int)
(assert (>= spent 0))
(assert (> amount 0))
(assert (>= limit spent))
(define-fun contract () Bool (<= amount (- limit spent)))
(define-fun implementation () Bool (<= (+ spent amount) limit))
; Ask for a legal input where the implementation disagrees with the contract.
(assert (not (= implementation contract)))
(check-sat)
; Expected: unsat. No such input exists within this model.