# z3 and z3PY giving different results

When I tried following in z3, I got result timeout

(set-option :smt.mbqi true) (declare-fun R(Int) Int) (declare-fun Q(Int) Int) (declare-var X Int) (declare-var Y Int) (declare-const k Int) (assert (>= X 0)) (assert (> Y 0)) (assert (forall ((n Int)) (=> (= n 0) (= (Q n) 0)))) (assert (forall ((n Int)) (=> (= n 0) (= (R n) X)))) (assert (forall ((n Int)) (=> (> n 0) (= (R (+ n 1) ) (+ (R n) (* 2 Y)))))) (assert (forall ((n Int)) (=> (> n 0) (= (Q (+ n 1) ) (- (Q n) 2))))) (assert (forall ((n Int)) (=> (> n 0) (= X (+ (* (Q n) Y) (R n)))))) (assert (forall ((n Int)) (= X (+ (* (Q n) Y) (R n))))) (assert (= X (+ (* (Q k) Y) (R k)))) (assert (not (= (* X 2) (+ (* (Q (+ k 1)) Y) (R (+ k 1)))))) (check-sat)

Same when I tried in z3py using following code, I got result unsat which is wrong

from z3 import * x=Int('x') y=Int('y') k=Int('k') n1=Int('n1') r=Function('r',IntSort(),IntSort()) q=Function('q',IntSort(),IntSort()) s=Solver() s.add(x>=0) s.add(y>0) s.add(ForAll(n1,Implies(n1==0,r(0)==x))) s.add(ForAll(n1,Implies(n1==0,q(0)==0))) s.add(ForAll(n1,Implies(n1>0,r(n1+1)==r(n1)-(2*y)))) s.add(ForAll(n1,Implies(n1>0,q(n1+1)==q(n1)+(2)))) s.add(x==q(k)*y+r(k)) s.add(not(2*x==q(k+1)*y+r(k+1))) if sat==s.check(): print s.check() print s.model() else : print s.check()

Looking forward to Suggestions.

## Answers

My suggestion is to use replace the built-in not operator by the Z3 function called Not, e.g.

not(2*x==q(k+1)*y+r(k+1))

is simplified to False by Python before Z3 gets to see it, while

Not(2*x==q(k+1)*y+r(k+1))

has the desired meaning.