Z3.wasm

(declare-fun x () Int) (declare-fun y () Int) (declare-fun z () Int) (assert (>= (* 2 x) (+ y z))) (declare-fun f (Int) Int) (declare-fun g (Int Int) Int) (assert (< (f x) (g x x))) (assert (> (f y) (g x x))) (check-sat) (get-model) (push) (assert (= x y)) (check-sat) (get-model) (check-sat) (pop) (exit)

Assembled by Clément Pit-Claudel by compiling Z3 with Emscripten.