Email Gateway (Aug 23 2022 at 08:47): Email Gateway (Aug 23 2022 at 08:47):From: Peter Lammich <lammich@in.tum.de>
Hi.
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.
Email Gateway (Aug 23 2022 at 08:49):From: Jasmin Blanchette via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi Peter,
I have already reported the "bad SMT term: _ " error from Z3,
The problem here is that bit vector reconstruction has never been implemented [*].
As for the CVC4 crash, I can reproduce it too on my Mac, but the issue appears to be solved in the latest version. I hope to rebuild new versions of most provers this year, in time for the next release.
Thanks for the report.
Jasmin
[*] despite the title "Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL" of a CPP 2011 publication...
but the
core dumps from CVC4 are new.--
Petertheory 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
donelemma 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)
/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 9893 /tmp/isabelle-
j65266pl/process1068846226209823883/cache-io-6417024 > /tmp/isabelle-
j65266pl/process1068846226209823883/cache-io-6417026 2>&1
/tmp/isabelle-j65266pl/process1068846226209823883/bash_script6418082:
line 1: 10946 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 9821 /tmp/isabelle-
j65266pl/process1068846226209823883/cache-io-6418078 > /tmp/isabelle-
j65266pl/process1068846226209823883/cache-io-6418080 2>&1
/tmp/isabelle-j65266pl/process1068846226209823883/bash_script6418808:
line 1: 10950 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 9740 /tmp/isabelle-
j65266pl/process1068846226209823883/cache-io-6418804 > /tmp/isabelle-
j65266pl/process1068846226209823883/cache-io-6418806 2>&1
/tmp/isabelle-j65266pl/process1068846226209823883/bash_script6419276:
line 1: 10954 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 9686 /tmp/isabelle-
j65266pl/process1068846226209823883/cache-io-6419272 > /tmp/isabelle-
j65266pl/process1068846226209823883/cache-io-6419274 2>&1
/tmp/isabelle-j65266pl/process1068846226209823883/bash_script6419566:
line 1: 10958 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 9629 /tmp/isabelle-
j65266pl/process1068846226209823883/cache-io-6419562 > /tmp/isabelle-
j65266pl/process1068846226209823883/cache-io-6419564 2>&1
/tmp/isabelle-j65266pl/process1068846226209823883/bash_script6419774:
line 1: 10963 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 9578 /tmp/isabelle-
j65266pl/process1068846226209823883/cache-io-6419770 > /tmp/isabelle-
j65266pl/process1068846226209823883/cache-io-6419772 2>&1
/tmp/isabelle-j65266pl/process1068846226209823883/bash_script6419980:
line 1: 10967 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 28609
/tmp/isabelle-j65266pl/process1068846226209823883/cache-io-6419976 >
/tmp/isabelle-j65266pl/process1068846226209823883/cache-io-6419978
2>&1
"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)*)
Last updated: Apr 26 2024 at 16:20 UTC