Fix z3.

diff --git a/2020-frama-c/4500-range-size-2.term b/2020-frama-c/4500-range-size-2.term
index 7c4b874..ecef5b8 100755 (executable)
--- a/2020-frama-c/4500-range-size-2.term
+++ b/2020-frama-c/4500-range-size-2.term
@@ -8,5 +8,6 @@ export title="qemu’s range_size()"
 # History.
 remember 'cat snippets/range_size.c'
 remember 'frama-c -wp -wp-rte snippets/range_size.c'
+remember 'frama-c -wp -wp-rte snippets/range_size.c -wp-prover alt-ergo,why3:z3-ce'
 
 terminal

diff --git a/2020-frama-c/notes.txt b/2020-frama-c/notes.txt
index 3dbe211..b7254f7 100644 (file)
--- a/2020-frama-c/notes.txt
+++ b/2020-frama-c/notes.txt
@@ -252,12 +252,17 @@ looks equally trivial and yet it cannot be proven.  Why?
 
 One way to find the problem would be to find a COUNTEREXAMPLE.  A
 counterexample is an instance of an input that satisfies all of the
-preconditions, but makes the postcondition false.  Now Frama-C has
+preconditions, but makes the postcondition false.  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 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).
+counterexamples.
+
+ $ frama-c -wp -wp-rte snippets/range_size.c -wp-prover alt-ergo,why3:z3-ce
+
+Unfortunately Z3 cannot find a counterexample in this case.  I even
+upped the timeout to run Z3 longer but it still couldn't find one.
+
+[Z3 model_compact issue: https://git.frama-c.com/pub/frama-c/-/issues/33]
 
 So this is the counterexample which I worked out myself: