3sum.smt2

; https://leetcode.com/problems/3sum-closest/

(declare-const a Int)
(declare-const b Int)
(declare-const c Int)

(assert (or (= a -1) (= a 2) (= a 1) (= a -4)))
(assert (or (= b -1) (= b 2) (= b 1) (= b -4)))
(assert (or (= c -1) (= c 2) (= c 1) (= c -4)))

(assert (< a b))
(assert (< b c))

(declare-const target Int)
(assert (= target 1))

(declare-const total Int)
(assert (= total (+ a b c)))

(minimize (abs (- target total)))

(check-sat)
(get-model)