From d52a4ce8b3084bfe5df4a7bd43293d4598a7e64c Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Thu, 15 Oct 2020 09:45:12 +0100 Subject: [PATCH] notes.txt: Add link to Z3 model_compress bug. --- 2020-frama-c/notes.txt | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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: -- 1.8.3.1