Microsoft Z3 import SMT file

Question

I want to use Z3 (version 4.5.0.1) with .net and wonder if i can use a SMTLIB file. So i have this simple smt file that i want to load in my program:

(declare-const x Int)
(declare-const y Int)
(assert (< x 4))
(assert (< (- y x) 1))
(assert (> y 1))

In c# i tryed the folowing:

using(Context context = new Context(new Dictionary<string, string>() { { "model", "true" } })) {
    context.ParseSMTLIB2String(Resources.SampleSMT2);
    var solver = context.MkOptimize();
    solver.Check();
    Console.WriteLine($"model: {solver.Model}"); // empty
    //BigInteger x = (solver.Model.Evaluate(...) as IntNum).BigInteger;
    //BigInteger y = (solver.Model.Evaluate(...) as IntNum).BigInteger;
}

But i dont know how to solve the problem provided in the smt file because in this example the model is empty.

Answer 1

ParseSMTLIB2String returns a BoolExpr that contains the assertions in the smt2 file, i.e., something like

BoolExpr be = context.ParseSMTLIB2String(...); solver.Add(be); solver.Check(); ...

should get you there.