Claude Marche
db96723fd9
fix sessions
2022-07-07 15:49:23 +02:00
Claude Marche
33115df1c9
fix sessions
2022-06-22 15:39:14 +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
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
Sylvain Dailler
1b71ca59c5
Update session and shapes
2019-05-20 17:09:01 +02:00
Sylvain Dailler
4fe56b451c
Update obsolete session
2019-05-07 18:49:07 +02:00
Claude Marche
c4366cb352
update sessions
2019-05-06 22:35:38 +02:00
Sylvain Dailler
01f3e01b6b
Fix obsolete session and coq proofs
2019-04-10 11:41:01 +02:00
Guillaume Melquiond
bcee782715
Update shapes.
2019-02-18 16:56:12 +01:00
DAILLER Sylvain
48793c5b03
Range projection meta
2018-10-30 19:23:34 +01:00
Sylvain Dailler
25411b404d
Update ce-bench and obsolete sessions
2018-10-24 12:38:38 +02:00
Sylvain Dailler
e27ff68eac
Update obsolete session
2018-10-23 14:50:59 +02:00
Claude Marche
47500c797b
update sessions
2018-10-16 16:57:08 +02:00
Jean-Christophe Filliatre
b8c5222cce
new example: binary_multiplication with 63-bit integers
2018-10-04 16:47:09 +02:00
Andrei Paskevich
1de56fdb50
update the shapes to v5 in regtests
...
not updated:
- stdlib/array - the proof is broken
- ring_decision/ - not replayed, proof broken
- in_progress/, util/, prover/bench/ - not replayed
2018-09-23 22:49:56 +02:00
Andrei Paskevich
5c35938dbe
upgrade to Alt-Ergo 2.0.0, CVC4 1.5, Z3 4.6.0, Eprover 2.0 where possible
2018-07-04 19:57:15 +02:00
Guillaume Melquiond
035ba52ec4
Clean some session files.
2018-04-04 11:50:21 +02:00
Claude Marche
5fb8c95fc1
update sessions and shapes after merge with master (improvements on shape computations)
2017-06-22 14:13:32 +02:00
Jean-Christophe Filliatre
3773922d3d
updated proof sessions
2017-05-16 14:01:57 +02:00
Jean-Christophe Filliatre
2ac91ce7e7
binary_multiplication: new-system-compliant code and a few comments
2016-06-02 17:00:43 +02:00
Andrei Paskevich
0f9ded381b
examples: reconstruct sessions
...
still problematic:
tests-provers/div
tests-provers/div_real
check-builtin/int
bts/fsetint
logic/bitvectors
logic/einstein
logic/genealogy
bitvectors/power2
bellman_ford
knuth_prime_numbers
vstte12_combinators
hoare_logic/blocking_semantics5
known issues:
- Timeout is not always recognized
- why3 tactic does not work: ENOENT on connect()
- temporary output files are created in the curdir
- temporary output files are sometimes not erased
- socket file is created in the curdir
2016-04-14 23:34:13 +02:00
