z3 reports unknown for decidable fragment with proof-production enabled
We have a (large) SMT-LIBv2 input file, using the QF_UFlogic fragment. Z3
is able to determine that the file is unsat in a few seconds. However,
when we turn on proof-production, z3 reports unknown after just a few
seconds and without using significant memory resources. When trying the
same file with a different solver (veriT), we are able to obtain a proof
(~500 KB) in just a few seconds.
As QF_UF is a decidable fragment, and also our file does not seem too
difficult, we are rather surprised by this result. Our best guess is that
z3 exhausts some sort of internal resource limit. So we have two
questions: Is there a way to find out why z3 gives up and reports unknown
(so quickly)? And if this is due to some internal limit, can this be
increased by some configuration setting?
No comments:
Post a Comment