;; Carries are 0 or 1
(declare-const c1 Int) (assert (&& (>= c1 0) (<= c1 1)))
(declare-const c2 Int) (assert (&& (>= c2 0) (<= c2 1)))
(declare-const c3 Int) (assert (&& (>= c3 0) (<= c3 1)))
;; All digits are in {0, 1, ... 9}
(declare-const f Int) (assert (&& (>= f 0) (<= f 9)))
(declare-const t Int) (assert (&& (>= t 0) (<= t 9)))
(declare-const u Int) (assert (&& (>= u 0) (<= u 9)))
(declare-const w Int) (assert (&& (>= w 0) (<= w 9)))
(declare-const r Int) (assert (&& (>= r 0) (<= r 9)))
(declare-const o Int) (assert (&& (>= o 0) (<= o 9)))
;; Arithmetic
(assert (= (+ o o) (+ r (* 10 c1))))
(assert (= (+ c1 (+ w w)) (+ u (* 10 c2))))
(assert (= (+ c2 (+ t t)) (+ o (* 10 c3))))
(assert (= c3 f))
;; First digits cannot be zero
(assert (not (= t 0)))
(assert (not (= f 0)))
;; Assumption: all digits are distinct
(assert (distinct f t u w r o))
(check-sat)
(get-model)
(exit)