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?
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)