How to get_unsat_core in Z3?

Question

I have the following python program.

from z3 import *
x = Bool("X")
y = Bool("Y")
s = Solver()
s.add(x==y)
s.add(x!=False)
s.add(y!=True)
s.check()

The last line gives output unsat. But how to print the unsat core of this?

Answer 1

You can ask for an unsat core as follows:

from z3 import *

#  https://z3prover.github.io/api/html/classz3py_1_1_solver.html#ad1255f8f9ba8926bb04e1e2ab38c8c15

x = Bool('X')
y = Bool('Y')
s = Solver()
s.set(unsat_core=True)

s.assert_and_track(x == y, 'a1')
s.assert_and_track(x != False, 'a2')
s.assert_and_track(y != True, 'a3')

result = s.check()
print(result)
if result == unsat : 
    c = s.unsat_core()
    print(len(c))
    print('a1 ', Bool('a1') in c)
    print('a2 ', Bool('a2') in c)
    print('a3 ', Bool('a3') in c)
    print(c)

Resulting output:

unsat
3
a1  True
a2  True
a3  True
[a1, a2, a3]

This is a trivial unsat core as it contains all assertions. Look at a related discussion.