Solène Moreau
|
74914e7651
|
(V719-014) Merging Inria/master into SPARK/master
Change-Id: I2144736b2dbb76966fbe4eae6238a8751799a3d2
Depends-On: I5a522521b64c6e676113695f30625b9618461867
Depends-On: I51bf388c10a7d73401ebb48c7c3c07828da4af12
|
2022-07-19 14:57:03 +02:00 |
|
MARCHE Claude
|
bec4f19215
|
Resolve "z3 driver should not unfold definitions"
|
2022-07-09 09:12:15 +00: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 |
|
Solène Moreau
|
4441127004
|
V516-003 Merging Inria master into SPARK master
Change-Id: I8cf967252c89e4cb3a31a0257060eee413f61f28
Depends-On: Ida46d9019fdc15a00df2697c45e5519b48bbe7aa
Depends-On: I710c21a3c22933eec6a2369ed6a293bb30b73bbf
|
2022-06-15 14:15:27 +02:00 |
|
Claude Marche
|
8abedf035e
|
fix sessions
|
2022-06-02 17:59:27 +02:00 |
|
Claude Marche
|
22c68ef4fe
|
update sessions
|
2022-05-24 11:34:40 +02:00 |
|
Nightly Build
|
9e5eb47599
|
Vc: keep sp_if's splittable (and update sessions)
|
2022-05-02 18:29:28 +02:00 |
|
Solène Moreau
|
a29b8b930c
|
V325-031 Merging Why3/Inria master into Why3/SPARK master
Change-Id: Ib12de95cfa922bd1b8c1f5ad1ba269de9c90894c
Depends-On: I3c3e37849899e4436210701c67ddf0049aa08204
Depends-On: I28a9ef2ea1b11448bea50d1f4c4c799e8255fda8
|
2022-04-26 09:17:30 +02:00 |
|
MARCHE Claude
|
c6f793011c
|
introduce_premises also "dequant" the let-ins
|
2022-04-21 16:23:20 +00:00 |
|
MARCHE Claude
|
bcfef9818c
|
Resolve "Fix drivers for SMT-LIB strings"
|
2022-04-06 14:29:41 +00:00 |
|
Solène Moreau
|
524b938a9d
|
V325-031 Merge with upstream Why3
Change-Id: I2e98bd5ec8c138751713811f4dad164be6a4463a
|
2022-03-29 10:47:33 +02:00 |
|
Claude Marche
|
47d57c2c39
|
update sessions
|
2022-03-25 15:49:33 +01:00 |
|
Claude Marche
|
e7efe033be
|
fix sessions
|
2021-10-30 11:11:24 +02:00 |
|
Benedikt Becker
|
d919886b0c
|
T127-015 Merge with upstream Why3
Change-Id: Ic6472dd67180667554db718c8f328f9832b1e8fb
|
2021-09-07 13:50:44 +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 |
|
Benedikt Becker
|
cda8f07ac9
|
Update example sessions
|
2021-06-03 12:38:14 +02:00 |
|
Benedikt Becker
|
aec68a1fc2
|
T127-015 Merge with upstream Why3
Change-Id: I7313db75ec835fc732ad8f6f40bc70dde659ff12
|
2021-05-18 09:40:47 +02:00 |
|
Quentin Garchery
|
235e8dede9
|
fix examples euler_sieve and multiprecision/mpz_mul
|
2021-04-29 12:44:16 +02:00 |
|
Andrei Paskevich
|
f4ca81247d
|
Repair discriminate2
|
2021-04-08 12:26:07 +00:00 |
|
Benedikt Becker
|
786a717c3a
|
T127-015 Merge with upstream Why3
Change-Id: Id74e07534977f55a4a5962d340d2645f043a9a81
|
2021-02-18 10:18:01 +01:00 |
|
Claude Marche
|
41e9cbc7d2
|
update obsolete sessions
|
2021-02-12 17:39:18 +01:00 |
|
Guillaume Melquiond
|
7574bfe84e
|
Clean standard library.
|
2021-01-29 18:34:19 +01:00 |
|