https://github.com/EasyCrypt/easycrypt
Revision 7d8a5132179c1bc4ef395f6ceb5d0f721e3542d8 authored by François Dupressoir on 10 October 2020, 11:22:49 UTC, committed by François Dupressoir on 10 October 2020, 12:08:14 UTC
These SMT fail when using: - Why3 1.3.1 - Z3 4.8.9 - CVC4 1.9 - Alt-Ergo 1.3.3 This appears to be bad interplay between the provers and this version of Why3: the proofs work with Why3 1.2
1 parent 469a12a
Tip revision: 7d8a5132179c1bc4ef395f6ceb5d0f721e3542d8 authored by François Dupressoir on 10 October 2020, 11:22:49 UTC
Help smt along in brittle proofs
Help smt along in brittle proofs
Tip revision: 7d8a513
File | Mode | Size |
---|---|---|
algebra | ||
analysis | ||
core | ||
crypto | ||
datatypes | ||
distributions | ||
encryption | ||
looping | ||
modules | ||
newth | ||
oldlibs | ||
prelude | ||
query_counting | ||
structure | ||
tactics |
Computing file changes ...