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! *)

Last updated: Sep 17 2026 at 22:43 UTC