title: Using define-fun-rec in SMT
body: <p>I'm currently trying to write an SMT script using define-fun-rec.  I've tested with both Z3, version 4.4.2, and CVC4, version 1.4.  As far as I can tell, these are the most recent versions of both, and both support the feature*.  However, both do not seem to recognize the command.</p>
  
  <p>(I made some changes to this based on Nikolaj's reply.  It still gives the error messages.)  Specifically, given:</p>
  
  <pre><code>(define-fun-rec 
      fac ((x Int)) Int
      (
          ite (&lt;= x 1) 
              1 
              (* x (fac (- x 1)))
      )
  )
  
  (assert (= (fac 4) 24))
  
  (check-sat)
  </code></pre>
  
  <p>Z3 outputs:</p>
  
  <pre><code>unsupported
  ; define-fun-rec
  (error "line 10 column 17: unknown function/constant fac")
  sat
  </code></pre>
  
  <p>And CVC4 outputs:</p>
  
  <pre><code>(error "Parse Error: fac.smt2:1.15: expected SMT-LIBv2 command, got `define-fun-rec'.
  
    (define-fun-rec 
     ^
  ")
  </code></pre>
  
  <p>My best guess is that there is some sort of flag I need to set or I need to be using some specific logic, but I've had a lot of trouble finding any sort of detailed instructions or examples with define-fun-rec.  Any advice would be appreciated.  Thanks!</p>
  
  <p>*Z3 has support: <a href="https://stackoverflow.com/questions/36431075/how-to-deal-with-recursive-function-in-z3">How to deal with recursive function in Z3?</a></p>
  
  <p>CVC4 has support: <a href="http://lara.epfl.ch/~reynolds/pres-smt15.pdf" rel="nofollow noreferrer">http://lara.epfl.ch/~reynolds/pres-smt15.pdf</a></p>