ada/why3
0
0
Fork 0
mirror of https://github.com/AdaCore/why3.git synced 2026-02-12 12:34:55 -08:00
Code Issues Packages Projects Releases Wiki Activity
18,511 Commits 65 Branches 1 Tag
master
Commit Graph

640 Commits

Author SHA1 Message Date
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
Guillaume Melquiond
ef4680ca53 Change detection order to favor recent versions of Vampire. 2025-04-02 10:57:01 +02:00
MARCHE Claude
25a128513d drivers for Alt-Ergo 2.6: FPA implicit, CE and BV 2024-10-08 15:11:12 +02:00
MARCHE Claude
33f94a61d4 Merge branch '880-add-support-for-alt-ergo-2-6-and-last-versions-of-z3-and-cvc5' into 'master' 
Resolve "Add support for Alt-Ergo 2.6 and last versions of Z3 and cvc5"

Closes #880

See merge request why3/why3!1137
 2024-10-03 14:24:06 +02:00
Claude Marche
e48d2d01de Support for Alt-Ergo 2.6.0 2024-10-03 11:32:26 +02:00
Claude Marche
27fb33580e Support for Coq 8.19.2 2024-10-03 11:19:54 +02:00
Claude Marche
cc2b44edeb Support for Z3 4.13 and cvc5 1.1 and 1.2 2024-10-03 09:47:17 +02:00
Paul Patault
bf775596c8 coma: generalize let%attr in let%span 
+ creusot patches
+ CI patches
 2024-08-08 11:09:30 +02:00
Paul Patault
ec40aa57b7 coma: WIP RE 2024-08-08 09:06:08 +02:00
Paul Patault
afe55f5fa8 coma: fix typing case lambda 2024-08-08 09:06:07 +02:00
Guillaume Melquiond
0ffca0b670 Recognize both 8.19 and 8.20 as supported versions of Coq. 2024-07-04 19:47:45 +02:00
Claude Marche
4d68a5a802 disabled Alt-Ergo FPA for versions < 2.5.4 (bug known) 2024-05-23 11:17:31 +02:00
Claude Marche
dce21458fe fix command line for Alt-Ergo 2.5.x FPA 2024-04-24 15:21:01 +02:00
Claude Marche
74c4013d95 restored legacy shortcuts for Alt-Ergo 2024-02-12 16:02:52 +01:00
Claude Marche
3e3ae13ff3 add use_at_auto_level for Alt-Ergo 2.5.x 2024-01-08 21:22:39 +01:00
BONNOT Paul
2410ff364d Added missing prover alternative FPA for Alt-Ergo 2.5.x 2024-01-08 20:14:24 +00:00
Guillaume Melquiond
4719d21c55 Mark Isabelle 2022 as supported. 2023-12-08 13:55:11 +01:00
MARCHE Claude
8815d4d0f3 support for Alt-Ergo with Dolmen front-end and SMT syntax 
for versions of Alt-Ergo >= 2.5.2

add Alt-Ergo in CE bench
 2023-11-16 19:34:49 +00:00
Guillaume Melquiond
25b9f61103 Adapt to Coq 8.18. 2023-11-13 14:51:18 +01:00
MARCHE Claude
0cd72486d6 Support for Alt-Ergo 2.5.1 2023-09-29 09:46:31 +00:00
BONNOT Paul
754be52d42 Support for Alt-Ergo 2.4.3 2023-08-22 08:58:18 +00:00
Guillaume Melquiond
64facc03bd Add support for Coq 8.17. 2023-04-04 15:47:58 +02:00
BONNOT Paul
8c839099bb max_int and max_real values not defined as an axiom 
Transform eliminate_big_constant for dReal prover
 2023-04-04 13:00:22 +00:00