From: Richard W.M. Jones Date: Thu, 15 Oct 2020 08:45:12 +0000 (+0100) Subject: notes.txt: Add link to Z3 model_compress bug. X-Git-Url: http://git.annexia.org/?a=commitdiff_plain;ds=inline;h=d52a4ce8b3084bfe5df4a7bd43293d4598a7e64c;p=libguestfs-talks.git notes.txt: Add link to Z3 model_compress bug. --- diff --git a/2020-frama-c/notes.txt b/2020-frama-c/notes.txt index d41e161..3dbe211 100644 --- a/2020-frama-c/notes.txt +++ b/2020-frama-c/notes.txt @@ -255,9 +255,9 @@ counterexample is an instance of an input that satisfies all of the preconditions, but makes the postcondition false. Now Frama-C has pluggable provers, and one prover called Z3, originally written by Microsoft, can be used with Frama-C and can sometimes find -counterexamples. However for some reason the version of Z3 in Fedora -does not like to work with the version of Frama-C in Fedora and I -don't know why. +counterexamples. However the version of Z3 in Fedora does not like to +work with the version of Frama-C in Fedora +(https://git.frama-c.com/pub/frama-c/-/issues/33). So this is the counterexample which I worked out myself: