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/bts
History
Claude Marche 6f2e594fa1 reproducer and fix
2025-09-29 18:16:21 +02:00
..
16_subst
add a meta to mark a symbol as never removed by remove_unused*
2023-06-15 15:18:48 +00:00
19_apply_with
add a meta to mark a symbol as never removed by remove_unused*
2023-06-15 15:18:48 +00:00
71_disambiguation
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
79_compute_unsound
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
114_infix
fix sessions and CE oracles
2024-11-14 14:48:30 +01:00
116_array_access
fix sessions and CE oracles
2024-11-14 14:48:30 +01:00
126_apply
add a meta to mark a symbol as never removed by remove_unused*
2023-06-15 15:18:48 +00:00
138
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
185_apply
add a meta to mark a symbol as never removed by remove_unused*
2023-06-15 15:18:48 +00:00
185_apply_let
fix sessions
2021-09-03 11:59:11 +02:00
231_destruct
Resolve "Remove axioms in Z3 and CVC4 drivers"
2023-09-01 15:47:33 +00:00
244_destruct_rec
fix sessions
2021-09-03 11:59:11 +02:00
264_destruct_if
fix obsolete sessions
2024-10-27 17:46:42 +01:00
265_apply
fix sessions
2021-09-03 11:59:11 +02:00
269_replace_under_if
add a meta to mark a symbol as never removed by remove_unused*
2023-06-15 15:18:48 +00:00
276_shape
add a meta to mark a symbol as never removed by remove_unused*
2023-06-15 15:18:48 +00:00
311_destruct
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
380_doc_trans
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
380_trans_space_args
fix sessions
2021-09-03 11:59:11 +02:00
438
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
450_abs
fix sessions and CE oracles
2024-11-14 14:48:30 +01:00
548-neg-float-lit
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
587
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
612
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
626
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
656
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
690_reserved_keywords
upgrade bench scripts with CVC5 from 1.0.0 to 1.0.5, upgrade sessions
2023-07-11 15:13:50 +02:00
695_remove_unused
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
742
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
746
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
753
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
773
Add metas for unused dependencies in generated axioms
2024-10-25 18:34:29 +02:00
788
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
886
fix sessions and CE oracles
2024-11-14 14:48:30 +01:00
926
reproducer and fix
2025-09-29 18:16:21 +02:00
12475
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
12934
Support for Coq 8.19.2
2024-10-03 11:19:54 +02:00
13375
Add a initial comment in shapes files
2021-08-25 10:49:04 +00:00
13849
Support for Coq 8.19.2
2024-10-03 11:19:54 +02:00
13853
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
13854
Support for Coq 8.19.2
2024-10-03 11:19:54 +02:00
16972
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
20445
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
ce_symbols
Resolve "Remove axioms in Z3 and CVC4 drivers"
2023-09-01 15:47:33 +00:00
destruct_term
fix obsolete sessions
2024-10-27 17:46:42 +01:00
fsetint
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
remove_unused_remove_cte
upgrade bench scripts with CVC5 from 1.0.0 to 1.0.5, upgrade sessions
2023-07-11 15:13:50 +02:00
16_subst.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
19_apply_with.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
71_disambiguation.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
79_compute_unsound.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
95_char_encoding_latin1.mlw
fix issue #95
2018-02-21 11:27:36 +01:00
101_eprover_eliminate_range_literal.mlw
remove useless import (avoid warnings)
2019-05-13 17:45:06 +02:00
114_infix.mlw
Add test for 114
2018-07-19 12:36:15 +02:00
116_array_access.mlw
Update example of issue 116
2018-07-19 14:53:34 +02:00
126_apply.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
130_extraction.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
138.mlw
Pmodule: clone range/float types correctly
2018-06-18 00:50:24 +02:00
185_apply_let.mlw
[transform apply] let is now a premise for applied condition of apply
2018-09-20 14:14:14 +02:00
185_apply.mlw
New test for apply
2018-10-26 16:30:40 +02:00
231_destruct.mlw
destruct: adhoc unsoundness correction
2018-11-29 16:42:13 +01:00
244_destruct_rec.mlw
example file for issue 244 destruct_rec
2018-12-07 09:42:08 +01:00
264_destruct_if.mlw
Update examples for recursive destruct of conditionals and matches
2019-02-08 12:41:28 +01:00
265_apply.mlw
apply test: add new tests for let.
2019-02-12 16:55:35 +01:00
269_replace_under_if.mlw
example for issue #269, can't reproduce
2019-02-12 10:35:20 +01:00
276_shape.mlw
Change the internal representation of shapes and shape files
2019-05-20 17:02:14 +02:00
306.mlw
Pmodule: t->t->t functions can be overloaded as X->X->t functions
2024-09-19 10:54:24 +02:00
311_destruct.mlw
avoid warning "axiom does not contains abstract local symbols"
2020-08-26 10:33:54 +02:00
353.mlw
cleaning
2020-08-25 13:33:36 +02:00
374_eliminate_if_explodes.mlw
cleaning
2020-08-25 13:33:36 +02:00
380_doc_trans.mlw
avoid warning "axiom does not contains abstract local symbols"
2020-08-26 10:33:54 +02:00
380_trans_space_args.mlw
transformation args: space immediately after ',' are not args separators
2019-10-28 15:30:55 +01:00
438.mlw
Add an alternative "FPA" to Alt-Ergo, supporting dedicated reasoning on floating-point and real numbers
2022-11-03 08:47:46 +00:00
450_abs.mlw
In SMTLIB, "abs" is *not* the absolute value on reals
2020-03-04 09:54:27 +01:00
548-neg-float-lit.mlw
fix recent change in bv theory : do not import useless ComputerDivision
2021-02-08 20:31:27 +01:00
559.mlw
keep attributes when converting between bool and prop
2022-07-22 12:39:45 +02:00
587.mlw
Parser accepts ident after variant
2023-04-04 12:34:26 +00:00
612.mlw
Add metas for unused dependencies in generated axioms
2024-10-25 18:34:29 +02:00
626.mlw
Changed the unsecure trusted_wf attribute mechanism into a more secure one
2023-02-22 13:50:29 +00:00
656.mlw
Add metas for unused dependencies in generated axioms
2024-10-25 18:34:29 +02:00
690_reserved_keywords.mlw
Resolve "CVC4 driver does not escape is"
2022-11-15 11:39:59 +00:00
695_remove_unused.mlw
Improve "remove_unused" transformation
2022-10-17 09:13:01 +00:00
742.mlw
Resolve "Attributes before a let in a formula are lost"
2023-04-30 09:09:25 +00:00
746.mlw
Add test for #746
2023-03-27 16:54:24 +02:00
747.mlw
fix closure computation in remove_unused
2024-10-22 21:25:49 +02:00
753.mlw
Add metas for unused dependencies in generated axioms
2024-10-25 18:34:29 +02:00
760.mlw
transparently import module wf when needed
2023-06-27 08:02:43 +02:00
773.mlw
Add metas for unused dependencies in generated axioms
2024-10-25 18:34:29 +02:00
788.mlw
Add test
2023-09-01 16:04:59 +02:00
842.mlw
take type variables instances into account in execution engine
2024-10-01 11:44:59 +02:00
886.mlw
add regression test from BTS
2024-11-13 19:04:53 +01:00
926.mlw
reproducer and fix
2025-09-29 18:16:21 +02:00
12445.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
12475.why
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
12934.why
A bit of cleaning
2011-07-04 15:58:15 +02:00
13002.why
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
13375.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
13515.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
13849.why
BTS 13849
2012-02-02 16:42:41 +01:00
13853.mlw
Generalization of check_unused_vars to logic and program decl
2019-08-20 15:48:44 +02:00
13853a.mlw
Generalization of check_unused_vars to logic and program decl
2019-08-20 15:48:44 +02:00
13853b.mlw
Generalization of check_unused_vars to logic and program decl
2019-08-20 15:48:44 +02:00
13854.why
simplify copyright headers
2012-10-20 15:43:52 +02:00
14097.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
16972.mlw
Update examples in progress
2016-03-09 15:22:02 +01:00
17137.mlw
details
2014-09-09 16:46:05 +02:00
17184.mlw
Fix occurrences of "occurences".
2023-11-23 19:04:11 +01:00
18953.why
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
20445.mlw
WhyML: "use/clone T" imports by default (in absence of "as")
2018-06-15 16:45:58 +02:00
20618.mlw
Merge branch 'master' into new_system
2016-08-18 17:22:04 +02:00
20619.mlw
examples from BTS
2016-11-16 08:51:31 +01:00
20881.why
Fix CR/LF encoding.
2020-03-27 11:10:47 +01:00
bts12244.ml
rename "split_goal" to "split_goal_wp" in session files
2014-09-04 21:08:44 +02:00
ce_symbols.mlw
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
destruct_term.mlw
destruct_term: do not ignore definitions introduced by types
2019-04-30 10:28:54 +02:00
execute.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
fsetint.why
stdlib: set library revamped
2019-03-07 11:13:49 +01:00
remove_unused_remove_cte.mlw
new meta to declare that a constant can be removed by remove_unused_keep_constant
2023-06-06 16:51:09 +00:00
simplify.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00