Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Sledgehammer errors (Isabelle 2020)

Email Gateway (Jan 03 2021 at 14:43):

From: Makarius <makarius@sketis.net>
On 21/04/2020 19:01, Peter Lammich wrote:

I get the following error when running sledgehammer on certain
statements. It seems to be reproducible on my machine, where I get the
same output each time.

I have already reported the "bad SMT term: _ " error from Z3, but the
core dumps from CVC4 are new.

theory Scratch
imports
"Word_Lib.Word_Lemmas"
begin
(* TODO: Move *)
lemma word1_neqZ_is_one: "(a::1 word) ≠ 0 ⟷ a=1"
apply transfer
subgoal for a
apply (cases "bin_last a")
by auto
done

lemma word1_cases[cases type]:
fixes a :: "1 word" obtains (zero) "a=0" | (one) "a=1"
apply (cases "a=0")
by (auto simp: word1_neqZ_is_one)

lemma "from_bool (to_bool a ∧ to_bool b) = a && b" for a b :: "1
word"
sledgehammer

(*

Sledgehammering...
Proof found...
/tmp/isabelle-j65266pl/process1068846226209823883/bash_script6413124:
line 1: 10915 Aborted (core dumped)
/home/j65266pl/opt/Isabelle2020/contrib/cvc4-1.5-5/x86_64-linux/cvc4 --
full-saturate-quant --inst-when\=full-last-call --inst-no-entail --
term-db-mode\=relevant --multi-trigger-linear --no-statistics --random-
seed\=1 --lang\=smt2 --continued-execution --tlimit 9990 /tmp/isabelle-
j65266pl/process1068846226209823883/cache-io-6413120 > /tmp/isabelle-
j65266pl/process1068846226209823883/cache-io-6413122 2>&1
/tmp/isabelle-j65266pl/process1068846226209823883/bash_script6417028:
line 1: 10942 Aborted (core dumped)
[...]
"cvc4": The prover crashed
"e": Try this: by (metis (full_types) from_bool_1 to_bool_0 to_bool_1
word1_neqZ_is_one word_bool_alg.conj_one_right word_log_esimps(1)) (119
ms)
"z3": A prover error occurred:
bad SMT term: _
"vampire": Try this: by (metis (full_types) from_bool_neq_0 to_bool_0
to_bool_1 word1_cases word_and_notzeroD word_bw_same(1)) (54 ms)

*)

Trying a variant of this example with Isabelle2021-RC1, I get soft failures
for the SMT tools, without hard crashes. This is for AFP/a31f698ef3f8:

Isabelle2021-RC1/bin/isabelle jedit -d afp-devel/thys Scratch.thy

I can't say if it is within the intended range of functionality or
non-functionality of the SMT tools with the HOL Word library.

Makarius
Scratch.thy

Email Gateway (Jan 03 2021 at 17:19):

From: Mathias Fleury <mathias.fleury12@gmail.com>
Thanks for revisiting that thread.

Trying a variant of this example with Isabelle2021-RC1, I get soft failures
for the SMT tools, without hard crashes. This is for AFP/a31f698ef3f8:

Isabelle2021-RC1/bin/isabelle jedit -d afp-devel/thys Scratch.thy

I can't say if it is within the intended range of functionality or
non-functionality of the SMT tools with the HOL Word library.

The Z3 errors are expected, the CVC4 are not. I am working on it -- CVC4
is producing warnings that are not properly ignored.

Mathias

Makarius

Last updated: Jul 15 2022 at 23:21 UTC