ada/why3
0
0
Fork 0
mirror of https://github.com/AdaCore/why3.git synced 2026-02-12 12:34:55 -08:00
Code Issues Packages Projects Releases Wiki Activity
Files
master
why3/examples/logic
History
Matteo Manighetti 7ae65be566 Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
..
agatha
Move CVC4 proofs to CVC5
2023-08-28 14:31:08 +02:00
bitvectors
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
bvsum
update sessions
2024-11-03 11:48:13 +01:00
distr
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
drinker
fix sessions
2021-09-03 11:59:11 +02:00
einstein
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
explicit_subst
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
ffx
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
First
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
genealogy
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
hello_proof
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
lagrange_inequality
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
los_problem
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
my_cosine
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
real
Support for Coq 8.19.2
2024-10-03 11:19:54 +02:00
scottish-private-club
Upgrade CVC3 proofs
2023-08-28 14:28:03 +02:00
simple
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
sorted_list
Support for Coq 8.19.2
2024-10-03 11:19:54 +02:00
triangle_inequality
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
agatha.why
reorganize examples/
2013-01-30 01:23:44 +01:00
bitvectors.why
update sessions
2018-10-16 16:58:10 +02:00
bvsum.mlw
cleaning
2020-08-25 13:33:36 +02:00
distr.why
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
drinker.mlw
make shapes loading more robust
2020-03-17 14:55:34 +01:00
einstein.why
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
explicit_subst.why
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
ffx.why
new example logic/ffx.why
2013-10-10 15:10:16 +02:00
First.why
a few more simple examples and tests
2014-08-26 14:47:48 +02:00
genealogy.why
reorganize examples/
2013-01-30 01:23:44 +01:00
hello_proof.why
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
isa_planner.why
Generalization of check_unused_vars to logic and program decl
2019-08-20 15:48:44 +02:00
lagrange_inequality.why
add a meta to mark a symbol as never removed by remove_unused*
2023-06-15 15:18:48 +00:00
los_problem.why
new logic example: Los problem
2014-02-04 10:35:59 +01:00
my_cosine.why
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
real.why
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
scottish-private-club.why
Use why3doc comments rather than why3 label for module documentation.
2018-01-12 18:05:43 +01:00
simple.why
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
sorted_list.why
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
triangle_inequality.why
Resolve "z3 driver should not unfold definitions"
2022-07-09 09:12:15 +00:00