[isabelle] MATCH exception on smt (verit), but works fine... · Mirror: Isabelle Users Mailing List

Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] MATCH exception on smt (verit), but works fine...

Email Gateway (Sep 10 2026 at 17:00):

From: Peter <cl-isabelle-users@lists.cam.ac.uk>
Subject: [isabelle] MATCH exception on smt (verit), but works fine without (verit)

Hi List,

sledgehammer gave me a proof (with a >1.0s, timeout) using smt (verit),
and it failed with a MATCH exception. Without the (verit) option, it
goes through in a few milliseconds.

Peter

theory Scratch
imports Complex_Main
begin

lemma log_b_0[simp]: "log 0 x = 0"
unfolding log_def by simp

lemma "0≤⌈log b n⌉" for b n :: nat
apply (smt (verit) ln_0 ln_one log_b_0 log_def of_nat_0
of_nat_le_0_iff one_of_nat_le_iff zero_le_ceiling zero_le_log_cancel_iff)
(* exception MATCH raised (line 284 of "pattern.ML") *)

apply (smt ln_0 ln_one log_b_0 log_def of_nat_0
of_nat_le_0_iff one_of_nat_le_iff zero_le_ceiling zero_le_log_cancel_iff)
(* No subgoals! *)

Email Gateway (Sep 22 2026 at 21:58):

From: Hanna Elif Lachnitt <cl-isabelle-users@lists.cam.ac.uk>
Subject: [isabelle] MATCH exception on smt (verit), but works fine without (verit)

Hi Peter,
Thanks for reporting this. I had looked into this example, and it turned out to be a bug in veriT's number printer, so I had passed it on to the veriT developers. The proof certificate veriT emits contains an equality between an integer and a real number, which is not allowed under the used proof standard.
The developers found that this bug has already existed in previous versions of veriT and therefore is not a regression but used to fail in a different way than now. Unfortunately, it is a little more complex to fix and will take some more time. The good news is that it should only occur in rare circumstances.
I will add better error messaging on the Isabelle side even though this case is really not something that we usually consider the responsibility of the ITP. I am also looking into why Sledgehammer suggested the proof if reconstruction failed.
Best,
Hanna

From: cl-isabelle-users-request@lists.cam.ac.uk <cl-isabelle-users-request@lists.cam.ac.uk>
Sent: Friday, September 11, 2026 05:04
To: cl-isabelle-users@lists.cam.ac.uk <cl-isabelle-users@lists.cam.ac.uk>
Subject: cl-isabelle-users Digest Fri, 11 Sep 2026 (1/1)

cl-isabelle-users digest Fri, 11 Sep 2026

Table of contents:

1 - [isabelle] MATCH exception on smt (verit), but works fine without
(verit) - Peter <p.lammich@utwente.nl>

Message-ID: <eb58bb19-72c9-4213-83f9-e997e591b0ee@utwente.nl>
Date: Thu, 10 Sep 2026 19:00:16 +0200
From: Peter <p.lammich@utwente.nl>
Subject: [isabelle] MATCH exception on smt (verit), but works fine without
(verit)