# [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.*