Why result of Z3 online and Z3PY are different?
<p>Following code I have tried in Online and Offline Z3</p>

<pre><code>(set-option :smt.mbqi true)
(declare-var X  Int)
(declare-var X_  Int)
(declare-var a_  Int)
(declare-var su_  Int)
(declare-var t_  Int)
(declare-var N1  Int)
(assert (&gt;= X 0))
(assert (forall ((n1 Int)) (=&gt; (&lt; n1 N1) (&gt;= X (* (+ n1 1) (+ n1 1))))))
(assert (= X_ X))
(assert (= a_ N1))
(assert (= su_ (* (+ N1 1) (+ N1 1))))
(assert (= t_ (* (+ N1 1) 2)))
(assert (&lt; X (* (+ N1 1) (+ N1 1))))
(assert  (not (&lt; X (* (+ a_ 1) (+ a_ 1)))))
(check-sat)
</code></pre>

<p>Result unsat</p>

<p>Following code I have tried in Z3PY</p>

<pre><code>set_option('smt.mbqi', True) 
s=Solver() 
s.add(X&gt;=0) 
s.add(ForAll(n1,Implies(n1 &lt; N1,((n1+1)**2)&lt;=X))) 
s.add(((N1+1)**2)&gt;X) 
s.add(X_==X) 
s.add(a_==N1) 
s.add(su_==((N1+1)**2)) 
s.add(t_==(2*(N1+1))) 
s.add(Not(((a_+1)**2)&gt;X))
</code></pre>

<p>result- unknown</p>

<p>Is processing power different?</p>