z3py unsat : proof() gives invalid usage and unsat core is empty

[YutanpoFR]

Dear all,

I use the z3py API, and wrote the following :

import z3
s = z3.Solver()
z3.set_param(proof=True)
s.add(unsatisfiable formula)
result = s.check()
if result == unsat :
    print s.proof()

And I get the following error :
z3.z3types.Z3Exception: invalid usage

I also try to get the unsat core, it is empty.

When the formula is satisfiable, the model generated is good.

Am I doing something wrong here ?

Thank you very much.
Yutanpo

[wintersteiger]

Thanks for reporting this issue. z3.set_param sets the global default option value, not the solver parameters. At least, we have to change the option before the solver object is created. However, there seems to be a problem with that too.

[YutanpoFR]

Than you for your answer.

Quick update :
I corrected the above script following your advice. The proof() uses way too much memory for my small machine. The assertions fits in few tens of thousand lines (~60 000 assertions), adding and solving them use around 200Mb while the proof uses more than the 4Gb I have on my machine.
Is there a way to make the proof use less memory ?
What about the unsat core that is empty ?

Thank you again,
Yutanpo

[wintersteiger]

Some very small problems are very hard to solve. Without further information I really can't tell whether your problems can be solved in less time or memory.

Note that enabling proof production can take the solver down completely different routes, because some simplifiers/preprocessors/tactics of Z3 do not implement proof production and consequently can't be used when proof production is enabled. Therefore, the problem that the solver sees may indeed be much harder and require more memory.

The unsat core being empty is expected, as unsat core production was not enabled and there are no tracked literals (see Solver.assert_and_track).