Commit Graph

71 Commits

Author SHA1 Message Date
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
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
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
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
f4ca81247d Repair discriminate2 2021-04-08 12:26:07 +00:00
Claude Marche
41e9cbc7d2 update obsolete sessions 2021-02-12 17:39:18 +01:00
benedikt becker
a5e42659e9 Update sessions and proofs 2021-01-15 15:02:37 +01:00
Jean-Christophe Filliatre
76cbd80b8c updated proof sessions 2021-01-13 11:37:22 +01:00
Andrei Paskevich
cf1cf2898c update sessions 2020-03-03 18:22:29 +01: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
DAILLER Sylvain
08857a1e85 Naming of ident: remove space in favor of "'"
- change prefix "mk " into suffix "'mk"
- change prefix "VC " into suffix "'VC"
2019-08-23 14:47:32 +02:00
Guillaume Melquiond
ac5b459da5 Update sessions. 2019-07-15 18:58:31 +02:00
Gabriel Scherer
8752f0dccb update examples/stdlib/array session files 2019-06-24 18:12:57 +02:00
Andrei Paskevich
5f725d4936 update sessions 2019-06-13 11:15:21 +02:00
Claude Marche
7ca0050d9e proof session: downgrade Coq 8.9.0 to 8.7.1 for replay on moloch 2019-06-07 15:56:19 +02:00