Matteo Manighetti
|
dabd0d669c
|
Merge attemp
|
2023-05-17 11:15:20 +02: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
|
5eef121a50
|
fix sessions
|
2023-04-09 18:33:02 +02: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 |
|
Johannes Kanig
|
41eac08831
|
Merging upstream Why3 into AdaCore master
|
2023-03-28 10:24:25 +09:00 |
|
MARCHE Claude
|
002a366469
|
need to eliminate_builtin before remove_unused
|
2023-03-06 22:20:36 +00:00 |
|
Solène Moreau
|
be1023970d
|
(W112-001) Merge Why3/master into SPARK
Change-Id: Iefffe9ad9367fbc1c590efdca96cf6311a02481d
Depends-On: If1f1bbd27aeeee421c8c6adb86fef670a924907a
Depends-On: I6be95441469218c8f9dfef8934764b92453c1727
|
2023-01-13 14:55:39 +01:00 |
|
Nightly Build
|
0f4686159f
|
update sessions
|
2022-10-07 12:40:08 +02:00 |
|
David Ewert
|
5f54fca95f
|
Add "remove_unused:dependency" to int.ComputerDivision
|
2022-09-21 20:15:46 +00:00 |
|
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 |
|