Hi, The following should be unsatisfiable but Z3 gives `sat` on it. ``` (declare-fun a () String) (declare-fun b () Int) (assert (> b 0)) (assert (= (int.to.str b) (str.++ "0" a))) (check-sat) ``` Revision: 05ad90c976be01b8dbd1e5025c819f405a3b49f5 OS: Ubuntu 18.04