Convert Microsoft Pex path conditions from Z3 native format to SMT-LIB

We talked before about getting the code path conditions from Microsoft Pex as in Z3 native format(.z3 file).

Sometimes you may need to convert from Z3 native format to SMT-LIB standard. You can do that using the Z3 C# APIs. The only trick here is: you have to use the Microsoft.Z3.dll that come with your current Microsoft Pex installation (C:\Program Files\Microsoft Pex\bin\Microsoft.Z3.dll).

To show how it works, let’s create a new C# console application. Add refeerence to Microsoft.Z3.dll that come with your Pex installation.

Edit your code to look like:

using System;
using System.IO;
using Microsoft.Z3;

namespace Z3ToSMTLIB
{
    class Program
    {
        static void Main(string[] args)
        {
            if(args.Length == 0)
                Console.WriteLine("Please provide input file name.");
            if (!File.Exists(args[0]))
                Console.WriteLine("The specified file doesn't exist.");
            using (Context ctx = new Context(new Config()))
            {
                string SMTLIB= ctx.ParseZ3File(args[0]).ToString();
                StreamWriter writer = new StreamWriter(args[0].TrimEnd("z3".ToCharArray()) + "SMTLIB");
                writer.Write(SMTLIB);
                writer.Close();
            }
        }
    }
}

Right click your project in the solution explorer and select Add >> New Item >> select Application Configuration File >> click Add. Edit the newly created App.config file to look like: Now you can run your code and pass a file in Z3 native format and get a file in SMT-LIB format. This SMT-LIB format opens a lot of possibilities that we will explore later.