Feasibility of quantified satisfaction techniques for CHC solving

[lastever-article]

I was trying to use the CHC solving engine of Z3. For example, to prove a contract of the McCarthy's 91 function,

def mc(x):
    if x > 100:
       return x - 10
    else:
       return mc(mc(x + 11))
# contract to be proved:  assert(x > 101 or mc(x) == 91)

I wrote the following code

s = SolverFor("HORN")
inv = Function('inv', IntSort(), IntSort(), BoolSort())
x, r, y, z = Ints('x r y z')
s.add(ForAll([x, r], Implies(And(x > 100, r == x - 10),  inv(x, r))))
s.add(ForAll([x, r, y, z], Implies(And(x <= 100, y == x + 11, inv(y, z), inv(z, r)),inv(x, r))))

s.add(ForAll([x, r], Implies(And(x <= 101, inv(x, r)), r <= 100)))

Z3 finds a solution for mc that is a sufficient invariant to establish the contract.

When I changed s = SolverFor("HORN") to s = SolverFor("UFLIA"), z3 cannon finish the solving for a long time.

However, I have also found that there are a few cases where s = SolverFor("UFLIA") (or s = SolverFor("UFBV"), etc) can be faster than the CHC engine.

Is there any theoretical or empirical guidance on the choice of the proper engine for the verification condition (VC) encodes as quantified formulas?
For example,

• It might be more convenient to encode the VC as quantified formulas that are not necessarily in the HORN fragment.
• Sometimes, even the VC is a HORN formula, the HORN engine (Spacer and BMC?) might not be the best choice.

Thanks!