git.annexia.org
/
libguestfs-talks.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
cdd812a
)
notes.txt: Add link to Z3 model_compress bug.
author
Richard W.M. Jones
<rjones@redhat.com>
Thu, 15 Oct 2020 08:45:12 +0000
(09:45 +0100)
committer
Richard W.M. Jones
<rjones@redhat.com>
Thu, 15 Oct 2020 08:45:12 +0000
(09:45 +0100)
2020-frama-c/notes.txt
patch
|
blob
|
history
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
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:
So this is the counterexample which I worked out myself: