[isabelle] z3 proof reconstruction failure



Hello,

when trying to proof the following (with z3):

lemma "x * y ≤ (0 :: int) ⟹ x ≤ 0 ∨ y ≤ 0"
by smt

I get a proof reconstruction failure:

Z3 found a proof, but proof reconstruction failed at the following subgoal:
  assumptions:
    x * y ≤ 0
    ¬ y ≤ 0
    ¬ x ≤ 0
  proposition: False
Adding a rule to the lemma group "z3_rule" might solve this problem.

I tried to add an appropriate lemma to the group z3_rule, but without success. Does anyone have an idea of how to make proof reconstruction succeed in this case?

-Matthias





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.