How to make z3 recognize equivalence of certain arithmetic expressions?

Question

I have a pretty simple problem, I'm mentioning the relevant part here:

;; All variables are declared to be of type Real

(assert (and (<= 1.0  var1-r) (< var1-r 4.0)))
;;following defines var1-r
(assert (= var1-r (+ a b)))
;;following defines var1-e
(assert (=> (and (<= 1.0 var1-r) (< var1-r 2.0)) (= var1-e 8388608.0)))
(assert (=> (and (<= 2.0 var1-r) (< var1-r 4.0)) (= var1-e 4194304.0)))
;;following defines var1
(assert (= var1 (/ (foo (* var1-r var1-e)) var1-e)))

;;Similarly for var2-r, var2-e, var2
(assert (and (<= 1.0  var2-r) (< var2-r 4.0)))
(assert (= var2-r (+ b a)))
(assert (=> (and (<= 1.0 var2-r) (< var2-r 2.0)) (= var2-e 8388608.0)))
(assert (=> (and (<= 2.0 var2-r) (< var2-r 4.0)) (= var2-e 4194304.0)))
(assert (= var2 (/ (foo (* var2-r var2-e)) var2-e)))

Here, foo() is a simple interpreted function, eg., foo (x) = (to_real (to_int x)) Note that var1 and var2 are equal. Reason: var1-r and var2-r are equal (commutativity of Reals) and consequently var2-e and var1-e are equal, leading to var1 and var2 being equal. However, I am not able to prove unsatisfiability of (not (= var1 var2)) using z3. In fact, the same is true if var2-r is defined as (+ a b). [Note that var1 and var2 being equal is actually also independent of the definition of foo()].

Answer 1

Please look at here. I am obtaining

unsat