Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] fast_lin_arith raises Fail

view this post on Zulip Email Gateway (Aug 22 2022 at 09:33):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
In the attached theory, auto first generates a number of warnings of the from

Linear arithmetic should have refuted the assumptions.
Please inform Tobias Nipkow.

before it crashes with an exception Fail
(line 503 of "~~/src/Provers/Arith/fast_lin_arith.ML"):
Linear arithmetic: failed to add thms

Tested with Isabelle2014 and Isabelle2015-RC1.

Best,
Andreas
Scratch.thy

Last updated: Nov 21 2024 at 12:39 UTC