# 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()
if sat==s.check():
print s.check()
print s.model()
else :
print s.check()
```

Looking forward to Suggestions.

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.