Fixed point solver's get_answer is not returning all the facts that were used in the derivation of query

[duttasridhar]

The below program queries for scenario_enabled, based on facts rule1, rule2, rule3.. If you look at the first answer in the output it doesnt return fact about rule2 that helped with the derivation of query.. I am not able to understand why this is happening. Appreciate any help with this.. Thanks!

from z3 import *
fp = Fixedpoint()
fp.set(engine='datalog')
fp.set('datalog.generate_explanations', True)
r = z3.BitVecSort(8)
scnario_enabled = z3.Function('scnario_enabled', r, r, r, z3.BoolSort())
rule1 = z3.Function('rule1', r, z3.BoolSort())
rule2 = z3.Function('rule2', r, z3.BoolSort())
rule3 = z3.Function('rule3', r, z3.BoolSort())
fp.register_relation(scnario_enabled, rule1, rule2, rule3)
a, b, c = z3.Consts('a b c', r)
fp.declare_var(a, b, c)
fp.rule(scnario_enabled(a, b, c), [
    rule1(a),
    rule2(b),
    rule3(c),
])
for i in range(20):
    fp.fact(rule1(i))
    fp.fact(rule2(i+1))
    fp.fact(rule3(i+2))
print(fp.query(scnario_enabled(a,b,c)))

def get_instructions(answers):
    for ans in answers.children():
        lastAnd = ans.children()[-1]
        trace = lastAnd.children()[-1]
        print_instructions(trace)
        print("===========================")
def print_instructions(exp):
    if len(exp.children()) == 0:
        print(str(exp.decl()).replace('<null>:\n', ''))
        return
    for child_exp in exp.children():
        print_instructions(child_exp)

get_instructions(fp.get_answer())

Output

rule3(#x15).
rule1(#x0c).
rule3(#x15).
===========================
rule3(#x15).
rule1(#x0c).
rule3(#x15).
===========================
rule3(#x15).
rule1(#x03).
rule3(#x15).
===========================
rule3(#x15).
rule1(#x0d).
rule3(#x15).
===========================