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

33 Commits

Author SHA1 Message Date
MARCHE Claude
89a894b47a do not map IEEE floats theory to Alt-Ergo's own theory 
Upgrade to AE 2.6.2
 2025-06-18 10:45:29 +09:00
Matteo Manighetti
8d9026f3ac Move CE oracles to Alt-Ergo 2.6.0 2024-12-06 16:09:37 +01:00
BONNOT Paul
617b6db4e6 Resolve "Remove axioms in Z3 and CVC4 drivers" 2023-09-01 15:47:33 +00:00
Matteo Manighetti
d31c53d53c Move CVC4 proofs to CVC5 2023-08-28 14:31:08 +02:00
Matteo Manighetti
bd4beefa5c Upgrade Z3 proofs 2023-08-28 14:29:51 +02:00
Matteo Manighetti
63fc2cfe55 Upgrade Alt-Ergo 2.0.0 proofs 2023-08-28 14:22:55 +02:00
Xavier Denis
87af5d805b Initial bulk upgrade of z3 2023-04-13 09:43:18 +00:00
MARCHE Claude
2f66628fa8 upgrade proofs with Z3 4.6.0 to 4.7.1 2023-04-07 09:37:36 +00:00
Claude Marche
75f8a9584a update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible 2023-04-05 13:48:22 +02:00
Claude Marche
33115df1c9 fix sessions 2022-06-22 15:39:14 +02:00
Claude Marche
62e1037ff1 fix sessions 2021-09-03 11:59:11 +02:00
Claude Marche
62d925e898 fix sessions 2021-06-25 10:26:57 +02:00
Guillaume Melquiond
dada254134 Update sessions. 2020-02-11 23:47:40 +01:00
Cláudio Belo Lourenço
a931ddb5a5 Sessions updated. 
In most cases the proof in CVC4 takes one step more than before due to
the why3 string built-in type. In a few cases the proof was updated.
 2019-10-29 22:37:11 +01:00
Sylvain Dailler
336a478250 Update session, ce-bench and coq files for "VC" -> "vc" in goal name 2019-10-11 21:01:43 +02:00
Sylvain Dailler
32d7cfe8de Rerun all sessions to update the file formats 
This also updates some of the "VC name" to "name'VC" that were never
updated.
 2019-09-24 17:58:31 +02:00
Sylvain Dailler
1b71ca59c5 Update session and shapes 2019-05-20 17:09:01 +02:00
Sylvain Dailler
4fe56b451c Update obsolete session 2019-05-07 18:49:07 +02:00
Claude Marche
c4366cb352 update sessions 2019-05-06 22:35:38 +02:00
Sylvain Dailler
25411b404d Update ce-bench and obsolete sessions 2018-10-24 12:38:38 +02:00
Sylvain Dailler
e27ff68eac Update obsolete session 2018-10-23 14:50:59 +02:00
Andrei Paskevich
1de56fdb50 update the shapes to v5 in regtests 
not updated:
- stdlib/array - the proof is broken
- ring_decision/ - not replayed, proof broken
- in_progress/, util/, prover/bench/ - not replayed
 2018-09-23 22:49:56 +02:00
Andrei Paskevich
bbd2dc4dce remove trivial goals from sessions 2018-09-23 19:19:16 +02:00
Andrei Paskevich
5c35938dbe upgrade to Alt-Ergo 2.0.0, CVC4 1.5, Z3 4.6.0, Eprover 2.0 where possible 2018-07-04 19:57:15 +02:00
Claude Marche
30fd6bb4a9 update obsolete sessions 2017-05-24 17:16:12 +02:00