Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] SMT proof fails with exception

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

From: Lars Hupel <hupel@in.tum.de>
(Isabelle2016-RC2)

Dear list,

I have a theorem on which I invoke Sledgehammer, but with "Try methods"
disabled. Sledgehammer succeeds and suggests 'smt'. But if I click on
the suggestion, I get:

exception THM 0 raised (line 89 of "goal.ML"):

Again, I can provide a theory which reproduces the problem.

Cheers
Lars

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

From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Please do so. Thanks.

Jasmin

Last updated: Nov 21 2024 at 12:39 UTC