Johannes Kanig
25b13e2cab
merge commit
2025-12-15 10:45:08 +09:00
MARCHE Claude
e42c43804e
Merge branch 'weekly_full_bench' into 'master'
...
Weekly full bench
See merge request why3/why3!1243
2025-12-11 23:21:29 +01:00
Claude Marche
9fb8f8f2c7
bench reduced using bench image with more provers
2025-12-11 18:25:13 +01:00
Benjamin Terra-Jorge
993ed183c1
Merge branch 'support-interfaces-in-parsing-api' into 'master'
...
Support interfaces in parsing api
See merge request why3/why3!1268
2025-12-11 16:53:06 +00:00
Claude Marche
d818a981f2
fix cmd line for E-prover 3.x
2025-12-11 16:29:16 +01:00
Claude Marche
1558726fcb
proper renaming of E prover 2.6
2025-12-11 13:58:58 +01:00
Claude Marche
2095b61181
eprover and spass and Z3 4.14
2025-12-11 12:03:25 +01:00
Claude Marche
0f40e89fbc
add E prover 2.6
2025-12-11 10:29:15 +01:00
Benjamin Terra-Jorge
8bb9da3b6b
Merge branch '894-extraction-broken-when-cloning-a-module-with-interface' into 'master'
...
Resolve "Extraction broken when cloning a module with interface"
Closes #894
See merge request why3/why3!1190
2025-12-10 09:20:51 +00:00
MARCHE Claude
5be96e2b3c
Merge branch 'improve_lse_hyps' into 'master'
...
relax hypothesis on a_max
See merge request why3/why3!1278
2025-12-09 11:58:17 +01:00
Claude Marche
9014bb8b92
update a session
2025-12-09 10:43:49 +01:00
Claude Marche
ef62a72810
more upgraded sessions
2025-12-09 10:43:49 +01:00
Claude Marche
8cff58bc24
fix mistake
2025-12-09 10:43:49 +01:00
Claude Marche
7620017bbf
upgraded provers in examples
2025-12-09 10:43:46 +01:00
Claude Marche
27884e1d27
more provers, replay restricted to real examples
2025-12-09 10:42:26 +01:00
Claude Marche
01f80d6f50
relax hypothesis on a_max
2025-12-08 16:19:47 +01:00
Jean-Christophe Filliatre
4bc892fd02
a better theory seq.Sum
...
do not sum the elements, but rather the application of a
function to the elements
2025-12-03 19:01:11 +01:00
MARCHE Claude
fdc76ccb86
Merge branch 'adjust_slse' into 'master'
...
improve proof of SLSE
See merge request why3/why3!1276
2025-12-02 09:54:06 +01:00
Claude Marche
66a8b29530
improve proof of SLSE
2025-12-02 08:50:44 +01:00
Andre Maroneze
9cb7ad7175
avoid iso-8859 encoding in examples
...
Used iconv -f iso-8859-1 -t utf-8 to convert some ISO-8859 files into UTF-8.
Reason: Debian's linter complains about non-utf8 encoding in installed
documentation files.
Note: file 'examples/bts/95_char_encoding_latin1.mlw' still contains iso-8859
encoding, but it is on purpose for testing. Debian does not complain about
that file, anyway.
2025-11-27 09:49:14 +01:00
MARCHE Claude
1b24286b35
Merge branch 'generalize_lse' into 'master'
...
Generalize proofs of LSE and SLSE to arbitrary float formats
See merge request why3/why3!1270
2025-11-25 12:34:29 +01:00
Claude Marche
fc857b2fc2
proved udivexact generique
2025-11-25 11:26:25 +01:00
Claude Marche
b9feb6aece
proved mul generique
2025-11-25 10:49:15 +01:00
Claude Marche
06c14de8b0
fixed slse proof
2025-11-24 17:21:15 +01:00
Claude Marche
7a655e6952
fixed lemma gg_bounds
2025-11-24 16:48:07 +01:00
