UNSAT Core C# API always empty

Mar 16, 2015 at 3:23 PM
Edited Mar 16, 2015 at 5:27 PM
I'm having troubles to find out the conflicting clauses from the solver. I have changed the proof property from the context into true. The UnsatCore property always gives me empty result. Here's a simple example to generate UNSAT result:
var settings = new Dictionary<string, string>() { { "proof", "true" } };
Context ctx = new Context(settings);
Solver solver = ctx.MkSolver();

var y = ctx.MkIntConst("y");
var one = ctx.MkInt(1);

BoolExpr constraint1 = ctx.MkBoolConst("Constraint1");
BoolExpr constraint2 = ctx.MkBoolConst("Constraint2");
solver.AssertAndTrack(ctx.MkEq(y, one), constraint1);    y == 1
solver.AssertAndTrack(ctx.MkGt(y, one), constraint2);    y > 1

var result = solver.Check();
if(result == Status.UNSATISFIABLE)
      foreach (Expr c in solver.UnsatCore)
           Console.WriteLine("{0}", c);
Any ideas would be appreciated!
Mar 17, 2015 at 12:37 PM
This was resolved by using UpdateParamValue to set the unsat_core parameter. There may still be a bug in the parameter setting infrastructure though, so if any other users experience similar issues, please report them here.