title: How to know which rules where used in the derivation of SAT result using fixed point engine of Z3?
body: <p>I'm using muZ engine of Z3. For all SAT cases I would like to see which rules where used in the derivation. Is there any way to extract this information?</p>
  
  <p>For instance the input might look like this:</p>
  
  <pre><code>(declare-rel R1 (Int))
  (declare-rel R2 (Int))
  (declare-rel q (Int))
  
  (declare-var n Int)
  
  (rule (R1 n) rule_one)
  (rule (=&gt; (R1 n) (R2 n)) rule_two)
  (rule (=&gt; (and (R2 n) (&lt; n 1)) (q n)) query)
  
  (query q
  :print-answer true
  )
  </code></pre>
  
  <p>And I'd be glad to know which rules were triggered, something like</p>
  
  <p>q is SAT, used rules: rule_one->rule_two->query</p>