title: Z3 ForAll on Arrays
body: <p>I have managed to create an Array of Records using Z3 but now am struggling to see the syntax I need to perform a $\forall$ operation on the Array... here is a snippet sample of the SMT-LIB2 code i have so far.</p>
  
  <pre><code>(declare-datatypes () ((rec (mk-R5 (age Int) (area Int) (married Bool)))))
  (declare-const recs (Array Int rec))
  (declare-const r1 rec)
  (assert(= (age r1) 15))
  (assert(= (area r1) 10001))
  (assert(= (married r1) true))
  (declare-const r2 rec)
  (assert(= (age r2) 35))
  (assert(= (area r2) 2845))
  (assert(= (married r2) true))
  (declare-const x Int)
  (declare-const y Int)
  (assert (= recs (store recs x r1)))
  (assert (= recs (store recs y r2)))
  (assert(forall ((i rec)) (= (married i) true)))
  (check-sat)
  (get-model)
  </code></pre>
  
  <p>I guess the third-last line should have some reference to the Array but I've tried everything and the tutorial did not help me with this problem. </p>
  
  <p>How do I perform a $\forall$ operation over the Array I have here?</p>