Can I get the path conditions from Pex in SMT 2 format?

Question

I'm using the z3_logdir and z3_loglevel environment variables to make Pex log the path conditions in *.z3 file formats. Is there a way to force pex to export the path conditions in SMT 2 format ? or convert the .Z3 file format to SMT 2 ?

Answer 1

Pex ships with the DLL for Z3: Microsoft.Z3.dll. This corresponds to Z3 version 2.5 (this can be downloaded from http://research.microsoft.com/en-us/um/redmond/projects/z3/old/older_z3.html). The API in Z3 v 2.5 contains parsing support for Z3 files into internal format and there are API functions for dumping these to SMT-LIB(1). Newer version of Z3 and other tools exist for converting SMT-LIB1 benchmarks to SMT-LIB2.