82 Commits

Author SHA1 Message Date
Claude Marche
2095b61181 eprover and spass and Z3 4.14 2025-12-11 12:03:25 +01:00
Matteo Manighetti
7ae65be566 Upgrade sessions to use Alt-Ergo 2.6.0 2025-01-14 19:48:35 +01:00
MARCHE Claude
9161acda8e Add metas for unused dependencies in generated axioms 2024-10-25 18:34:29 +02:00
Jacques-Henri Jourdan
1b9ff7667a Fix session timings on moloch 2023-10-23 09:18:45 +02:00
BONNOT Paul
2444f6c60a Remove axiom CompatOrderMult from Int theory of CVCx and Z3 drivers. 2023-09-07 18:05:01 +00:00
BONNOT Paul
617b6db4e6 Resolve "Remove axioms in Z3 and CVC4 drivers" 2023-09-01 15:47:33 +00:00
Matteo Manighetti
bd4beefa5c Upgrade Z3 proofs 2023-08-28 14:29:51 +02:00
Matteo Manighetti
92d760c7a4 Upgrade CVC3 proofs 2023-08-28 14:28:03 +02:00
Matteo Manighetti
63fc2cfe55 Upgrade Alt-Ergo 2.0.0 proofs 2023-08-28 14:22:55 +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
Xavier Denis
87af5d805b Initial bulk upgrade of z3 2023-04-13 09:43:18 +00: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
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
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
Nightly Build
9e5eb47599 Vc: keep sp_if's splittable (and update sessions) 2022-05-02 18:29:28 +02:00
Claude Marche
62e1037ff1 fix sessions 2021-09-03 11:59:11 +02:00
Benedikt Becker
b1a3e81a8b Update sessions 2021-08-04 10:31:28 +02:00
Claude Marche
e449b99c44 fix sessions 2021-06-25 14:15:38 +02:00
Claude Marche
6883e782f3 fix sessions 2021-06-25 11:29:41 +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