# HG changeset patch # User nipkow # Date 1685796864 -36000 # Node ID 0a098088745bcc3b83cc81d0c57d5563d90eceb6 # Parent 177dae28697b66d0e15e3f7f7666706347831b1f TN has enough examples of the bug. diff -r 177dae28697b -r 0a098088745b src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Fri Jun 02 12:14:17 2023 +0200 +++ b/src/Provers/Arith/fast_lin_arith.ML Sat Jun 03 22:54:24 2023 +1000 @@ -499,8 +499,7 @@ (tracing (cat_lines (["Assumptions:"] @ map (Thm.string_of_thm ctxt) asms @ [""] @ ["Proved:", Thm.string_of_thm ctxt fls, ""])); - warning "Linear arithmetic should have refuted the assumptions.\n\ - \Please inform Tobias Nipkow.") + warning "Linear arithmetic should have refuted the assumptions but failed to.") in finish ctxt' hyps fls end handle FalseE (thm, hyps, ctxt') => trace_thm ctxt ["False reached early:"] (finish ctxt' hyps thm)