Email Gateway (Nov 21 2020 at 05:56): Email Gateway (Nov 21 2020 at 05:56):From: Peter Reitinger <peter.reitinger@gmail.com>
Hi,
sorry for recently reporting just confusing behavior because of
polymorphism as a bug.
But this time, I am very sure to have observed a bug, if creation of a
memory dump characterizes a bug. ;-)
First the screenshot:
[image: image.png]
The theory reproducing this bug is attached. The try at the end of the
experimental proof (sorry about the mess there, I am still experimenting
with Word & Co theories) produces the error.
Best regards
Peter Reitinger
image.png
Show_bug2.thy
Email Gateway (Nov 21 2020 at 12:03):From: Makarius <makarius@sketis.net>
On 21/11/2020 06:56, Peter Reitinger wrote:
sorry for recently reporting just confusing behavior because of
polymorphism as a bug.But this time, I am very sure to have observed a bug, if creation of a memory
dump characterizes a bug. ;-)
The "bug" terminology does not make much sense beyond a certain complexity of
systems (or rather a multi-system compound like the Isabelle ecosystem). You
do have a large space that is "inhabitable", but you also have uncharted areas
where things don't work.
First the screenshot:
image.png
I recommend to copy paste actual source text and output, unless this is a
problem of GUI rendering or interaction.
The relevant part of the error is this:
/home/makarius/lib/Isabelle2020/contrib/z3-4.4.0pre-3/x86_64-linux/z3
smt.random_seed\=1 smt.refine_inj_axioms\=false -T:10 -smt2
/tmp/isabelle-makarius/process1270985018603270244/cache-io-3287480 >
/tmp/isabelle-makarius/process1270985018603270244/cache-io-3287482 2>&1
So this is a hard crash of the (rather old) version of z3 that we are using.
There have been other z3 inconveniences before, but I guess we can't upgrade
it easily.
Maybe an expert on the Isabelle/z3 can say more about the situation.
Makarius
Email Gateway (Nov 23 2020 at 03:23):From: Peter Reitinger <peter.reitinger@gmail.com>
Hi again,
maybe this helps...
Here I could produce a crash in "cvc4" with modified Word_Examples:
theory Word_Examples
imports Word_Bitwise
begin
(* commented previous lemmas out *)
lemma "slice 3 (0b101111::6 word) = (0b101::3 word)" by simp
(* BEGIN preitinger *)
declare [[show_sorts]]
lemma "takefill False (size (1::6 word) - (3::nat)) (to_bl (1::6 word)) =
[False, False, False]"
apply sledgehammer
Sledgehammering...
/tmp/isabelle-peter/process3745657003709610034/bash_script3287864: Zeile 1:
6505 Abgebrochen (Speicherabzug geschrieben)
/home/peter/isabelle/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-peter/process3745657003709610034/cache-io-3287858 >
/tmp/isabelle-peter/process3745657003709610034/cache-io-3287860 2>&1
/tmp/isabelle-peter/process3745657003709610034/bash_script3292002: Zeile 1:
6520 Abgebrochen (Speicherabzug geschrieben)
/home/peter/isabelle/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 9845
/tmp/isabelle-peter/process3745657003709610034/cache-io-3291998 >
/tmp/isabelle-peter/process3745657003709610034/cache-io-3292000 2>&1
/tmp/isabelle-peter/process3745657003709610034/bash_script3298144: Zeile 1:
6618 Abgebrochen (Speicherabzug geschrieben)
/home/peter/isabelle/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 3923
/tmp/isabelle-peter/process3745657003709610034/cache-io-3298140 >
/tmp/isabelle-peter/process3745657003709610034/cache-io-3298142 2>&1
/tmp/isabelle-peter/process3745657003709610034/bash_script3298666: Zeile 1:
6626 Abgebrochen (Speicherabzug geschrieben)
/home/peter/isabelle/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 3827
/tmp/isabelle-peter/process3745657003709610034/cache-io-3298662 >
/tmp/isabelle-peter/process3745657003709610034/cache-io-3298664 2>&1
"e": Timed out
"cvc4": The prover crashed
"z3": Timed out
"vampire": Timed out
Email Gateway (Nov 23 2020 at 07:49):From: Manuel Eberl <eberlm@in.tum.de>
Just a hunch, did you get your Isabelle distribtion from the official
website or from a package repository (e.g. installed using apt, pacman,
etc.)?
Manuel
Email Gateway (Nov 23 2020 at 08:15):From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi all,
I had a look and the problems comes from the generated SMT file. CVC4
does not accept a type annotation in the generated problem (and returns
a nice error message), while Z3 accepts it.
I don't know enough about the SMT-lib format to know who is right, but I
have asked experts to see which solver is wrong.
Thanks for reporting,
Mathias
Email Gateway (Nov 23 2020 at 10:13):From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi all,
Some explanation on the bug. The SMT-Lib format makes it possible to
write (_ bv4 9) to mean 4 :: 9 word. However, if the word does not fit,
like for 3 :: 1 word, it is not clear what this means.
If the solver accepts it, it has to discard the leftover bits
(truncating the number). But the SMT-Lib format is not explicit about
that and CVC4 rejects the problem file.
The solution is to generate 1:: 1 word (corresponding to _bv1 1) instead
of 3 :: 1 word (corresponding to _bv3 1).
I am currently testing a fix for that.
Mathias
Email Gateway (Dec 16 2020 at 08:53):From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi all,
the problem is now fixed
(https://isabelle-dev.sketis.net/rISABELLEf9424ceea3c33538bd3e52a12d9f8225c8256738).
Best,
Mathias
Email Gateway (Jan 02 2021 at 10:40):From: Makarius <makarius@sketis.net>
Can you try this again with current Isabelle2021-RC1
https://isabelle.in.tum.de/website-Isabelle2021-RC1 ?
It will require to change the Word setup: the NEWS file contains some hints
about that.
Makarius
Email Gateway (Jan 24 2021 at 19:29):From: Makarius <makarius@sketis.net>
Did you try anything in the meantime?
We already have https://isabelle.sketis.net/website-Isabelle2021-RC3 and
approx. 3 weeks left until everything becomes final and unchangeable.
(Isabelle releases don't have "patch-levels" after the deadline.)
Makarius
Last updated: Jan 04 2025 at 20:18 UTC