z3 - Z3 ソルバーが 2^x=4 を解けないのは普通ですか?

Question

Z3 の Web サイトに次の情報を掲載して、Z3 で 2^x=4 を解決しようとしました: https://rise4fun.com/z3/tutorial。

(declare-const x Real) 
(declare-const y Real) 
(declare-const z Real) 
(assert (=(^ 2 x) 4)) 
(check-sat) 
(get-model)

Z3プロデュース

unknown
(model 
)

Z3 を誤用していませんか?