"unknown sort" error in fixed point queries
<p>I am getting the "unknown sort" error when trying to pose a fixed point query using the <code>query</code> keyword.  For example, the following example from the fixed point tutorial, which works fine in the online version of Z3,</p>

<pre><code>(declare-rel mc (Int Int))
(declare-var n Int)
(declare-var m Int)
(declare-var p Int)

(rule (=&gt; (&gt; m 100) (mc m (- m 10))))
(rule (=&gt; (and (&lt;= m 100) (mc (+ m 11) p) (mc p n)) (mc m n)))

(query (and (mc m n) (&lt; n 91))
 :print-certificate true)
</code></pre>

<p>returns: </p>

<pre><code>(error "line 9 column 13: unknown sort 'mc'")
</code></pre>

<p>when I run it from the command line.  I use Z3 version 4.4.2 compiled from the github repository on Linux. My command line is: <code>z3 -smt2 example.smt</code></p>

<p>Are there some compilation flags I need to set to enable this functionality?</p>