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 (file)
--- 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: