title: How to deal with recursive function in Z3?
body: <pre><code>(set-option :smt.mbqi true)
  (declare-fun R(Int) Int)
  (declare-const a Int)
  (assert (= (R 0) 0))
  (assert (forall ((n Int)) (=&gt; (&gt; n 0) (= (R n ) (+ (R (- n 1)) 1)))))
  (assert (not (= a 5)))
  (assert (not (= (R a) 5)))
  (check-sat)
  </code></pre>
  
  <p>I have tried the above code in Z3,But Z3 unable to answer.Can you please guide me where i have made the mistake ?</p>