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.