How To Convert Z3py Expression To Smtlib 2 Format

My question is related to: Z3: convert Z3py expression to SMT-LIB2? I am trying to convert z3py expression from to smtlib2 format. using following script, but after conversion whe

Solution 1:

This is also related to another question here.

Most likely, this problem is because of an outdated version of Z3. There have been numerous bugfixes which haven't made it into the master branch yet and using the unstable branch (or the precompiled nightly binaries here) I get a different output, which is accepted by Z3 without errors:

(set-info :status unknown)
(set-logic QF_LIA)
(declare-funy()Int)
(declare-funx()Int)
(assert
(let (($x34 (= x (* 2 y))))
(let (($x31 (< x 100000)))
(let (($x10 (> x 0)))
(and $x10 $x31 $x34)))))
(check-sat)