search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.42k stars 1.47k forks source link

smtlib2 file generated by z3 API cannot be parsed by other SMT solvers #1133

Closed rainoftime closed 7 years ago

rainoftime commented 7 years ago

Hi~ When I dump constarints(encoded with z3 C++ API) to smtlib2 file and try to solve them with Boolector, some symbols cannot be recognized by Boolector. For example, boolector returns the error:

bv_case.smt2:10454:220723: undefined symbol 'bvsdiv_i'

Does z3 use additional symbols beyond smtlib2?

bv_case.txt

wintersteiger commented 7 years ago

Yes, Z3 supports more than SMT. This particular symbol is used to indicate the function bvsdiv, for the case that the divisor is non-zero and this symbol is introduced by the simplifier. E.g. calling the simplify tactic on the goal before sending it to another solver may not work out of the box. In this particular case, the easiest way to get rid of bvsdiv_i by replacing it by and if-then-else that checks whether the divisor is non-zero (in which case bvsdiv works fine), or else returns an uninterpreted constant.

See also https://github.com/Z3Prover/z3/issues/1132, https://github.com/Z3Prover/z3/commit/465ed7d068938d5b87cd8ede517f0e93b4ffe67f#commitcomment-22935595

NikolajBjorner commented 7 years ago

Z3 performs the rewrite: (bvsdiv x y) into (ite (= y 0) (bvsdiv_0 x) (bvsdiv_I x y))

So you can extract Boolector friendly semantics by replacing bvsidiv_i by bvsdiv and (bsdiv_0 x) by (bsdiv x 0) for suitable bit-widths.

Z3 does not pretend to have any guarantees of producing SMT2 compliant output as it also supports several non-standard extensions beyond these.