Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2020-RC4: Internal error from sledgeha...

Email Gateway (Aug 23 2022 at 08:47):

From: Makarius <makarius@sketis.net>
Thanks. This should work better with the following change:
https://isabelle.sketis.net/repos/isabelle-release/rev/8ed68b2aeba1

Somehow I have the impression that you are one of very few serious testers of
Isabelle2020 release candidates. That will become final and unchangeable in
approx. 10 days, so everybody else is called to start testing now.

Makarius

Email Gateway (Aug 23 2022 at 08:48):

From: Peter Lammich <lammich@in.tum.de>
Hi,

I've been running RC2 for the last weeks, without problems.
Now switched to RC4.
On both, sledgehammer sometimes shows errors like the following. Not
sure whether this is related.

Email Gateway (Aug 23 2022 at 08:49):

From: Makarius <makarius@sketis.net>
On 05/04/2020 00:22, Peter Lammich wrote:

I've been running RC2 for the last weeks, without problems.
Now switched to RC4.
On both, sledgehammer sometimes shows errors like the following. Not
sure whether this is related.

Thanks for continued testing of release candidates --- before Isabelle2020
becomes final on 15-Apr-2020 and cannot be changed anymore.

theory Scratch
imports
"HOL-Word.Word"
begin

lemma "(max_word::1 word) = 1"
sledgehammer
...
"z3": A prover error occurred:
bad SMT term: _

This appears to be an old problem of the SMT setup, it also occurs e.g. in
Isabelle2019, Isabelle2018, Isabelle2014.

I have created a task on our new isabelle-dev hosting platform to improve it
eventually (after the Isabelle2020 release): https://isabelle-dev.sketis.net/T20

Makarius

Email Gateway (Aug 23 2022 at 08:59):

From: Dominique Unruh <unruh@ut.ee>
Hi,

when running the attached example theory (using image HOL), sledgehammer
gives the following error:

"cvc4": A prover error occurred:
exception THEORY raised (line 971 of "thm.ML"):
  solve_constraints: bad theories for theorem
  (⋀x. (⋀x A f. x ∈ A ⟹ f x ∈ f A) ⟹ x ∈ written T ⟹ False) ⟹   (written T = {})   {..., HOL.Filter, HOL.Conditionally_Complete_Lattices, HOL.Binomial, Main, Draft.Error:108}   {..., HOL.Filter, HOL.Conditionally_Complete_Lattices, HOL.Binomial, Main, Draft.Error:97} "z3": A prover error occurred: exception THEORY raised (line 971 of "thm.ML"):   solve_constraints: bad theories for theorem   (⋀x. (⋀x A f. x ∈ A ⟹ f x ∈ f A) ⟹ x ∈ written T ⟹ False) ⟹
  (written T = {})
  {..., HOL.Filter, HOL.Conditionally_Complete_Lattices, HOL.Binomial,
Main, Draft.Error:108}
  {..., HOL.Filter, HOL.Conditionally_Complete_Lattices, HOL.Binomial,
Main, Draft.Error:97}

Best wishes,
Dominique.
Error.thy

Last updated: Apr 26 2024 at 08:19 UTC