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

24 Commits

Author SHA1 Message Date
Matteo Manighetti
7ae65be566 Upgrade sessions to use Alt-Ergo 2.6.0 2025-01-14 19:48:35 +01:00
Claude Marche
2e1d53f51b fix sessions and CE oracles 2024-11-14 14:48:30 +01:00
MARCHE Claude
9161acda8e Add metas for unused dependencies in generated axioms 2024-10-25 18:34:29 +02:00
MARCHE Claude
85916f62c6 never encode enums and records for Alt-Ergo 2024-05-22 12:18:37 +02:00
Loïc Correnson
e2afddb11d Resolve "Add injectivity for type invariant" 2024-01-31 13:02:13 +00:00
BONNOT Paul
2444f6c60a Remove axiom CompatOrderMult from Int theory of CVCx and Z3 drivers. 2023-09-07 18:05:01 +00:00
BONNOT Paul
617b6db4e6 Resolve "Remove axioms in Z3 and CVC4 drivers" 2023-09-01 15:47:33 +00:00
Matteo Manighetti
eddcb30d72 Update Alt-Ergo 2.3.x proofs 2023-08-28 14:17:52 +02:00
BONNOT Paul
29c71dbd51 add a meta to mark a symbol as never removed by remove_unused* 
mark some lemmas on division of real as removable if not needed
 2023-06-15 15:18:48 +00:00
David Ewert
5f54fca95f Add "remove_unused:dependency" to int.ComputerDivision 2022-09-21 20:15:46 +00:00
Claude Marche
db96723fd9 fix sessions 2022-07-07 15:49:23 +02:00
Claude Marche
8abedf035e fix sessions 2022-06-02 17:59:27 +02:00
Claude Marche
e7efe033be fix sessions 2021-10-30 11:11:24 +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
Andrei Paskevich
d2fb0befca examples: recompute broken v6 shapes 2020-08-26 19:32:11 +02:00
Claude Marche
fe71a8682d fix proof using another prover 2020-08-26 10:34:25 +02:00
Jean-Christophe Filliatre
86b7a7c78a updated proof sessions 2020-07-14 16:32:25 +02:00
Cláudio Belo Lourenço
2bf2f06f96 Update sessions using string theory. 2020-06-23 09:11:55 +02:00
Cláudio Belo Lourenço
424586aaa9 Update sessions 2020-04-03 12:30:03 +01:00
Cláudio Belo Lourenço
affea82b75 Fixes in base64 ane hex encoding 2020-02-24 16:16:39 +01:00
Jean-Christophe Filliatre
b13bca590c updated proof sessions using strings 2020-02-20 15:28:46 +01:00
Cláudio Belo Lourenço
d5cb482a25 Moving provable lemmas into string theory as axioms 2020-02-12 16:08:42 +01:00
Cláudio Belo Lourenço
99b8d3fa46 Spliting encoding into two files 2020-02-12 15:19:54 +01:00