Re: [isabelle] Issue with smt and linear arithmetic
linarith works as follows: Based on a decomposition of the original problem into a set of linear inequalities, it tries to find a refutation for them. The trace for the refutation is used to replay the steps, which should yield the Theorem False in the end. Proof replay essentially applies the simplifier with a carefully selected simpset. Whenever the final theorem differs from False, the warning you noticed is shown.
In your particular case, the obvious simplification for â(2x +2y) / 2â is not performed, because some rule or simproc is missing in linarithâs simpset. Extending the simpset appropriately would be a solution. Iâll see what I can do, such that your issue is resolved in the next release of Isabelle.
Von: Lukas Bulwahn
This archive was generated by a fusion of
Pipermail (Mailman edition) and