title: Is it expensive for z3 to solve a constraint set with quantifiers?
body: <p>I am using z3 (v4.3.1) to solve a constraint set containing uninterpreted functions with quantifiers. The problem is that the memory usage of z3 is very high. Below is my constraint:</p>
  
  <pre><code>(solver
  (v0 0)
  (forall ((i Int))
  (let ((a!1 (=&gt; (v0 i)
                 (and (not (v1 i))
                      (not (v2 i))
                      (not (v3 i))
                      (not (v4 i))
                      (not (v5 i))))))
    (=&gt; (&gt;= i 0) a!1)))
  (forall ((i Int)) (=&gt; (&gt;= i 0) (=&gt; (v0 i) (v1 (+ i 1)))))
  (forall ((i Int))
  (let ((a!1 (=&gt; (v1 i)
                 (and (not (v0 i))
                      (not (v2 i))
                      (not (v3 i))
                      (not (v4 i))
                      (not (v5 i))))))
    (=&gt; (&gt;= i 0) a!1)))
  forall ((i Int))
  (let ((a!1 (=&gt; (v1 i) (or (v2 (+ i 1)) (v5 (+ i 1))))))
    (=&gt; (&gt;= i 0) a!1)))
  (forall ((i Int))
  (let ((a!1 (=&gt; (v2 i)
                 (and (not (v0 i))
                      (not (v1 i))
                      (not (v3 i))
                      (not (v4 i))
                      (not (v5 i))))))
    (=&gt; (&gt;= i 0) a!1)))
  (forall ((i Int)) (=&gt; (&gt;= i 0) (=&gt; (v2 i) (v3 (+ i 1)))))
  (forall ((i Int))
  (let ((a!1 (=&gt; (v3 i)
                 (and (not (v0 i))
                      (not (v1 i))
                      (not (v2 i))
                      (not (v4 i))
                      (not (v5 i))))))
    (=&gt; (&gt;= i 0) a!1)))
  (forall ((i Int)) (=&gt; (&gt;= i 0) (=&gt; (v3 i) (v4 (+ i 1)))))
  (forall ((i Int))
  (let ((a!1 (=&gt; (v4 i)
                 (and (not (v0 i))
                      (not (v1 i))
                      (not (v2 i))
                      (not (v3 i))
                      (not (v5 i))))))
    (=&gt; (&gt;= i 0) a!1)))
  (forall ((i Int)) (=&gt; (&gt;= i 0) (=&gt; (v4 i) (v1 (+ i 1)))))
  (forall ((i Int))
  (let ((a!1 (=&gt; (v5 i)
                 (and (not (v0 i))
                      (not (v1 i))
                      (not (v2 i))
                      (not (v3 i))
                      (not (v4 i))))))
    (=&gt; (&gt;= i 0) a!1)))
  (forall ((i Int)) (=&gt; (&gt;= i 0) (=&gt; (v5 i) (v5 (+ i 1)))))
  (exists ((i Int)) (=&gt; (&gt;= i 0) (v5 i)))
  (forall ((i Int))
  (let ((a!1 (not (v5 (- (+ i 3) 1)))))
  (let ((a!2 (=&gt; (and (v0 i) (v1 (+ i 1))) a!1)))
    (=&gt; (&gt;= i 0) a!2))))
  (forall ((i Int))
  (let ((a!1 (not (v5 (- (+ i 4) 1)))))
  (let ((a!2 (=&gt; (and (v3 i) (v4 (+ i 1)) (v1 (+ i 2))) a!1)))
  </code></pre>
  
  <p>When I write the constraint set into a smt2 file and use z3 to solve it, I get the result "unknow" quickly. Below is content of the smt2 file</p>
  
  <pre><code>(declare-fun v0 (Int) Bool)
  (declare-fun v1 (Int) Bool)
  (declare-fun v2 (Int) Bool)
  (declare-fun v3 (Int) Bool)
  (declare-fun v4 (Int) Bool)
  (declare-fun v5 (Int) Bool)
  (assert (v0 0))
  (assert  (forall ((i Int)) (=&gt; (v0 i)     (and (not (v1 i)) (not (v2 i)) (not (v3 i))    (not (v4 i)) (not (v5 i))))))
  (assert  (forall ((i Int)) (=&gt; (v1 i)     (and (not (v0 i)) (not (v2 i)) (not (v3 i))   (not (v4 i)) (not (v5 i))))))
  assert  (forall ((i Int)) (=&gt; (v2 i)     (and (not (v1 i)) (not (v0 i)) (not (v3 i)) (not (v4 i)) (not (v5 i))))))
  (assert  (forall ((i Int)) (=&gt; (v3 i)     (and (not (v1 i)) (not (v2 i)) (not (v0 i)) (not (v4 i)) (not (v5 i))))))
  (assert  (forall ((i Int)) (=&gt; (v4 i)     (and (not (v1 i)) (not (v2 i)) (not (v3 i)) (not (v0 i)) (not (v5 i))))))
  (assert  (forall ((i Int)) (=&gt; (v5 i)     (and (not (v1 i)) (not (v2 i)) (not (v3 i)) (not (v4 i)) (not (v0 i))))))
  (assert  (forall ((i Int)) (=&gt; (&gt;= i 0) (=&gt; (v0 i) (v1 (+ i 1))))))
  (assert  (forall ((i Int)) (=&gt; (&gt;= i 0) (=&gt; (v1 i) (or (v2 (+ i 1)) (v5 (+ i 1)))))))
  (assert  (forall ((i Int)) (=&gt; (&gt;= i 0) (=&gt; (v2 i) (v3 (+ i 1))))))
  (assert  (forall ((i Int)) (=&gt; (&gt;= i 0) (=&gt; (v3 i) (v4 (+ i 1))))))
  (assert  (forall ((i Int)) (=&gt; (&gt;= i 0) (=&gt; (v4 i) (v1 (+ i 1))))))
  (assert  (forall ((i Int)) (=&gt; (&gt;= i 0) (=&gt; (v5 i) (v5 (+ i 1))))))
  (assert  (exists ((i Int)) (=&gt; (&gt;= i 0) (v5 i))))
  (assert (forall ((i Int)) (=&gt; (&gt;= i 0) (=&gt; (and (v0 i) (v1 (+ i 1))) (not (v5 (+ i 2)))))))
  (assert (forall ((i Int)) (=&gt; (&gt;= i 0) (=&gt; (and (v3 i) (v4 (+ i 1)) (v1 (+ i 2))) (not (v5 (+ i 3)))))))
  (check-sat)
  </code></pre>
  
  <p>I just wonder whether I write something wrong or the problem is hard for z3 to solve.</p>