rule of 3

(define-fun div3 ((i Int)) Bool
  (= (mod i 3) 0)
)

(define-fun-rec sumit ((i Int)) Int
     (ite (< i 10)
          i
          (+ (mod i 10) (sumit (div i 10))))
)

(declare-const x Int)
(assert (> x 0))
(assert (not (= (div3 x) (div3 (sumit x)))))
(check-sat)
(get-model)