Z3 uses many heuristics to control quantifier instantiation. One one them is based on the "instantiation depth". Z3 tags every expression with a "depth" attribute. All user supplied assertions are tagged with depth 0. When a quantifier is instantiated, the depth of the new expressions is bumped. Z3 will not instantiate quantifiers using expressions tagged with a depth greater than a pre-defined threshold. In your problem, the threshold is reached: (p 40)
is depth 0, (p 39)
is depth 1, (p 38)
is depth 2, etc.
To increase the threshold, you should use the option:
(set-option :qi-eager-threshold 100)
Here is the example with this option: http://rise4fun.com/Z3/ZdxO.
Of course, using this setting, Z3 will timeout, for example, for (p 110)
.
In the future, Z3 will have better support for "bounded quantification". In most cases, the best approach for handling this kind of quantifier is to expand it. With the programmatic API, we can easily "instantiate" expressions before we send them to Z3. Here is an example in Python (http://rise4fun.com/Z3Py/44lE):
p = Function('p', IntSort(), BoolSort())
s = Solver()
s.add(p(0))
s.add([ p(x+1) == p(x) for x in range(40)])
s.add(Not(p(40)))
print s.check()
Finally, in Z3, patterns containing arithmetic symbols are not very effective. The problem is that Z3 preprocess the formula before solving. Then, most patterns containing arithmetic symbols will never match. For more information on how to use patterns/triggers effectively, see this article. The author also provides a slide deck.