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
17,624 Commits 65 Branches 1 Tag
25.2
Commit Graph

40 Commits

Author SHA1 Message Date
Guillaume Melquiond
733973e9ab Remove some trailing whitespaces. 2023-11-23 18:46:29 +01:00
Jacques-Henri Jourdan
28369ea1c3 Fix sessions for nightly bench. 2023-10-22 15:49:03 +02: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
d31c53d53c Move CVC4 proofs to CVC5 2023-08-28 14:31:08 +02:00
Claude Marche
9451890c1f updated sessions 2023-08-24 16:29:59 +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
MARCHE Claude
715fa89d16 separate transformations for intros, dequant, and remove_unused 
remove unused before reflection transformation

avoid subst to a unused symbol
 2023-04-25 12:20:08 +00:00
Xavier Denis
87af5d805b Initial bulk upgrade of z3 2023-04-13 09:43:18 +00:00
Claude Marche
4ed431a8d3 new python example selection sort 2023-03-08 10:39:55 +01:00
Claude Marche
91a8a26fde fix obsolete sessions and one failed session 2023-02-07 12:25:21 +01:00
David Ewert
5f54fca95f Add "remove_unused:dependency" to int.ComputerDivision 2022-09-21 20:15:46 +00:00
Guillaume Melquiond
4d2d1c7183 Merge branch 'bugfix/v1.5' 2022-09-12 20:04:13 +02:00
Jean-Christophe Filliatre
f95a5214f6 fixed Python example and proof session 2022-09-09 14:56:11 +02:00
Jean-Christophe Filliatre
c891d2b87f updated proof sessions 2022-09-08 16:00:29 +02:00
Claude Marche
db96723fd9 fix sessions 2022-07-07 15:49:23 +02:00
Claude Marche
ecb497d98a Merge branch 'master' into eliminate_unused_symbols 2022-06-23 07:51:51 +02:00
Claude Marche
33115df1c9 fix sessions 2022-06-22 15:39:14 +02:00
Claude Marche
8abedf035e fix sessions 2022-06-02 17:59:27 +02:00
Nightly Build
9e5eb47599 Vc: keep sp_if's splittable (and update sessions) 2022-05-02 18:29:28 +02:00
MARCHE Claude
c6f793011c introduce_premises also "dequant" the let-ins 2022-04-21 16:23:20 +00:00
Jean-Christophe Filliatre
f31498beda fixed Python lexer 
empty comment lines were not accepted by the lexer
 2021-12-09 08:48:51 +01:00
Jean-Christophe Filliatre
6efdd5c9d5 micro-Python: new example 2021-12-06 10:34:17 +01:00
Claude Marche
e7efe033be fix sessions 2021-10-30 11:11:24 +02:00
Jean-Christophe Filliatre
08712c15ac micro-Python: added support for built-in function pow 2021-10-29 15:57:14 +02:00