title: list concat in z3
body: <p>Is there a way to concat two lists in z3? Similar to the @ operator in ML? I was thinking of defining it myself but I don't think z3 supports recursive function definitions, i.e., </p>
  
  <pre><code>define-fun concat ( (List l1) (List l2) List 
     (ite (isNil l1) (l2) (concat (tail l1) (insert (head l1) l2)) )
  )
  </code></pre>