; The same contract and preconditions as correct.smt2.
(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)))
; BUG: < rejects the valid payment that exactly reaches the limit.
(define-fun implementation () Bool (< (+ spent amount) limit))
(assert (not (= implementation contract)))
(check-sat)
(get-value (spent amount limit))
; Expected: sat, followed by a counterexample with spent + amount = limit.