I have the following query that works:
(set-info :status unknown)
(declare-fun n () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(assert (= 0 (mod c 2))) ; c is even
(assert (= b (div c 2))) ; b = c/2
(assert (not (= c (* 2 b)))) ; c != 2*b
(check-sat)
As expected I get unsat. However if I substitute c with (n * (n+1)) I get unknown(local z3 built from commit 5068d2083dc0609801f572a0e3d14df753d36a03, roughly 4.5.1) or timeout(on http://rise4fun.com/Z3):
(set-info :status unknown)
(declare-fun n () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(assert (= 0 (mod (* n (+ 1 n)) 2)))
(assert (= b (div (* n (+ 1 n)) 2)))
(assert (not (= (* n (+ 1 n)) (* 2 b))))
(check-sat)
Any idea why in one case it figures it out but not in the other?
Thanks! ~Dimo
When you put in n * (n+1) the problem becomes non-linear. (Non-linear means you multiply/divide by a non-constant.)
In such cases, the default solver is unlikely to produce a result, since the decision algorithms are only for the linear fragment of the logic. You are essentially at the mercy of heuristics: If they can solve your problem, great; if not, you get an unknown for answer.
Having said that, you can use "strategies" to guide the solver. In this case, the following seems to work:
(check-sat-using (and-then qfnra-nlsat smt))
With this, z3 successfully returns unsat for your query.
See http://rise4fun.com/z3/tutorial/strategies for details. It's an art to know what strategy would work for which problem, but if you read through the tutorial you can get a good sense of what to try.