how to convert z3py expression to smtlib 2 format

Question

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 when I am feeding the result to z3 or any other SMT, I get:

"Syntax error, unexpected let"

Is there any way that I can bring it in the smtlib2 format using z3py so that I dont have to write long expression again.

Following is the code which I am using for conversion:

def convertor(f, status="unknown", name="benchmark", logic=""):
v = (Ast * 0)()
if isinstance(f, Solver):
a = f.assertions()
if len(a) == 0:
  f = BoolVal(True)
else:
  f = And(*a)
return Z3_benchmark_to_smtlib_string(f.ctx_ref(), name, logic, status, "", 0, v, f.as_ast())

x = Int('x')
y = Int('y')
s = Solver()
s.add(x > 0)
s.add( x < 100000)
s.add(x==2*y)
print convertor(s, logic="QF_LIA")

and this is the output:

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

Christoph Wintersteiger Christoph Wintersteiger · Accepted Answer · 2014-03-24T22:03:07

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-fun y () Int)
(declare-fun x () Int)
(assert
(let (($x34 (= x (* 2 y))))
(let (($x31 (< x 100000)))
(let (($x10 (> x 0)))
(and $x10 $x31 $x34)))))
(check-sat)

how to convert z3py expression to smtlib 2 format

1 Answers