MARCHE Claude
89a894b47a
do not map IEEE floats theory to Alt-Ergo's own theory
...
Upgrade to AE 2.6.2
2025-06-18 10:45:29 +09:00
Matteo Manighetti
8d9026f3ac
Move CE oracles to Alt-Ergo 2.6.0
2024-12-06 16:09:37 +01:00
MARCHE Claude
9161acda8e
Add metas for unused dependencies in generated axioms
2024-10-25 18:34:29 +02:00
Jacques-Henri Jourdan
28369ea1c3
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
BONNOT Paul
617b6db4e6
Resolve "Remove axioms in Z3 and CVC4 drivers"
2023-09-01 15:47:33 +00:00
Matteo Manighetti
63fc2cfe55
Upgrade Alt-Ergo 2.0.0 proofs
2023-08-28 14:22:55 +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
David Ewert
5f54fca95f
Add "remove_unused:dependency" to int.ComputerDivision
2022-09-21 20:15:46 +00:00
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
Jean-Christophe Filliatre
49626575fa
updated proof sessions on moloch
2021-01-13 12:02:58 +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
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
DAILLER Sylvain
ebd8d5c6d2
Model record
2019-02-01 17:08:46 +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
22ab5177bb
fix issue #188
...
the beginner transformation `split_vc` is now using `introduce_premises`
followed by `subst_all`, instead of `simplify_trivial_quantification`
followed by `introduce_premises`.
following Andrei's suggestion, instead of `subst_all` we instead substitute
only the symbols that (1) were introduced earlier and (2) do not have
any attributes `[@model...]` so as to keep symbols present in the initial
code.
2018-10-02 16:55:13 +02:00
