(declare-fun a (Int Int Int) Int)
(declare-fun b (Int Int Int) Int)
(declare-fun c (Int Int Int) Bool)
(declare-fun d () Int)
(assert
(let ((aa (a d d d)))
(let ((e (a aa d d)))
(let ((f (div (~ 3) aa)))
(let ((i (~ f)))
(let ((g (* 3 e)))
(let ((h (- 214 g aa)))
(let ((l (~ g)))
(let ((j (- i)))
(let ((k (- i l)))
(let ((p (* 4 h)))
(let ((q (div i 0)))
(let ((m (~ d)))
(let ((n (b aa aa i)))
(let ((o (* 4 g)))
(let ((r (~ o)))
(let ((af (ite (c 3 0 3) 1 93)))
(let ((ag (distinct e p)))
(let ((ah (> aa k)))
(let ((ai (c q g 0)))
(let ((aj (c d aa 0)))
(let ((ak (= r i)))
(let ((al (= f 0)))
(let ((am (= m j)))
(let ((ao (> n h)))
(let ((ap (>= n g)))
(let ((aq (ite am aa af)))
(let ((ar (ite am i o)))
(let ((as (ite ag g o)))
(let ((ax (ite al m as)))
(let ((at (ite ao r 0)))
(let ((au (ite ai l 0)))
 (and (distinct
       (xor ak (xor aj (< as (ite ap ax at))))
       (distinct (ite al au 0) ar))
  (< (ite ah e af) aq))))))))))))))))))))))))))))))))))
(check-sat)

[664] % z3 small.smt2
sat
[665] % z3debug small.smt2
unsat
[666] % 
[666] % cat small.smt2
(declare-fun a (Int Int Int) Int)
(declare-fun b (Int Int Int) Int)
(declare-fun c (Int Int Int) Bool)
(declare-fun d () Int)
(assert
(let ((aa (a d d d)))
(let ((e (a aa d d)))
(let ((f (div (~ 3) aa)))
(let ((i (~ f)))
(let ((g (* 3 e)))
(let ((h (- 214 g aa)))
(let ((l (~ g)))
(let ((j (- i)))
(let ((k (- i l)))
(let ((p (* 4 h)))
(let ((q (div i 0)))
(let ((m (~ d)))
(let ((n (b aa aa i)))
(let ((o (* 4 g)))
(let ((r (~ o)))
(let ((af (ite (c 3 0 3) 1 93)))
(let ((ag (distinct e p)))
(let ((ah (> aa k)))
(let ((ai (c q g 0)))
(let ((aj (c d aa 0)))
(let ((ak (= r i)))
(let ((al (= f 0)))
(let ((am (= m j)))
(let ((ao (> n h)))
(let ((ap (>= n g)))
(let ((aq (ite am aa af)))
(let ((ar (ite am i o)))
(let ((as (ite ag g o)))
(let ((ax (ite al m as)))
(let ((at (ite ao r 0)))
(let ((au (ite ai l 0)))
 (and (distinct
       (xor ak (xor aj (< as (ite ap ax at))))
       (distinct (ite al au 0) ar))
  (< (ite ah e af) aq))))))))))))))))))))))))))))))))))
(check-sat)