Empty Unsat Cores when using Tactics in z3

Question

Solver returns empty unsat core when using tactics.

Case 1:

s = Solver()
x = Real('x')
B = Bool('b')
C = Bool('c')
s.add(B == (x > 1))
s.add(C == (x == -1))
s.check(B, C)

Case 2:

s = Then('simplify', 'solve-eqs', 'smt').solver()
x = Real('x')
B = Bool('b')
C = Bool('c')
s.add(B == (x > 1))
s.add(C == (x == -1))
s.check(B, C)

In both the cases, the check returns unsat (as it should), but I get an empty unsat core in the second case where I use tactics. Is there any way to get unsat core when using solvers with tactics?

PS: These are really simple examples for demonstration. I am working on a bigger problem where I have a number of LRA constraints (where tactics might be helpful) and I need to extract the unsat cores.

Answer 1

You need to explicitly enable unsat cores if you're using tactics. The following works:

from z3 import *
s = Then('simplify', 'solve-eqs', 'smt').solver()
s.set(unsat_core=True)
x = Real('x')
B = Bool('b')
C = Bool('c')
s.add(B == (x > 1))
s.add(C == (x == -1))
s.check(B, C)

print s.unsat_core()

Note the call to s.set on the third line. Output:

$ python b.py
[b, c]