slavchev

;; https://iobservable.net/blog/2017/12/27/playing-with-z3-theorem-prover/
;; https://rise4fun.com/Z3/E8DL

(define-fun Mul5 ((x Int)) Int (* x 5))
(define-fun Sub6 ((x Int)) Int (- x 6))
(define-fun Append4 ((x Int)) Int
    (ite (< x 0) (- (* x 10) 4) (+ (* x 10) 4))
)

(declare-fun s1Mul5 () Int)