"unknown sort" error in fixed point queries

Question

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

(declare-rel mc (Int Int))
(declare-var n Int)
(declare-var m Int)
(declare-var p Int)

(rule (=> (> m 100) (mc m (- m 10))))
(rule (=> (and (<= m 100) (mc (+ m 11) p) (mc p n)) (mc m n)))

(query (and (mc m n) (< n 91))
 :print-certificate true)

returns:

(error "line 9 column 13: unknown sort 'mc'")

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: z3 -smt2 example.smt

Are there some compilation flags I need to set to enable this functionality?

Answer 1

I recently changed the format of "query" to use a predicate only. The tutorial will have to be updated.

 (declare-rel q (Int Int))
 (rule (=> (and (mc m n) (< n 91)) (q m n)))
 (query q :print-certificate true)