1

Closed

Solver push/pop causes check to fail

description

I found a situation where simply performing a solver.push(); solver.pop() pair (even with nothing between) causes a later call to solver.check to return unknown rather than sat. I was able to reduce the test case as far as:
http://rise4fun.com/Z3Py/iAkW
Currently, this test returns unknown with the reason "(incomplete quantifiers)". However, without the "s.push(); s.pop()" on line 28, the call to s.check() returns sat (my actual code of course does more work between the push and pop, but it wasn't necessary for the test case). This happens on both the master and unstable branches.
Closed Jun 6, 2013 at 8:24 PM by leodemoura
This is not a bug, but a limitation of the current version. We can continue the discussion in the "Discussions Tab"

comments

amdragon wrote Mar 7, 2013 at 6:27 PM

I was able to reduce the test case further and eliminate the first quantifier expression, leaving only the quantifier that causes check to return unknown:
http://rise4fun.com/Z3Py/hwCV
As before, simply commenting out the "s.push(); s.pop()" on line 17 causes check to return sat.

leodemoura wrote Mar 7, 2013 at 7:35 PM

This is not a bug. Your formula is not in a fragment that can be decided by Z3.,
The Z3 tutorial describes some of the fragments that can be decided by Z3.
For satisfiable formulas containing quantifiers, Z3 builds the models using the MBQI (model based quantifier instantiation) module. For formulas that are not in a supported fragment, Z3 may fail to build the model an return unknown.
The push(); pop() may look like a "skip()" but it is not. It will change the way Z3 "compiles" the formulas into the its internal data-structures.

Without push();pop(), Z3 just got "lucky" and found the model even if the formula is not in one of the supported fragments.

That being said, we are always extending the fragments that can be decided automatically.

amdragon wrote Mar 8, 2013 at 2:33 PM

Thanks for the quick response and explanation.

My original problem may be more addressable. My code used to break the "fsdir" tuple into separate Z3 constants "_valid" and "_map", rather than bundling them into a datatype, so that the final quantifier looked more like
Not(Exists(fn,
           And(_valid[fn],
               Store(_map, dstb, _map[srcb])[fn] == _map[dstb])))
Based on my (certainly rudimentary) understanding, I don't think this is a decidable fragment either, but Z3 was always able to return an answer, even with assertion stack operations and far more assertions thrown into the mix. But this is the same formula, simply with constants in place of projections of a constant. Is it possible Z3 could recognize that the projections can be eliminated, or am I simply too far outside decidable fragment territory?

(Full example at http://rise4fun.com/Z3Py/ks9Q .)

Thank you for your time (and for Z3!)