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
18,511 Commits 65 Branches 1 Tag
master
Commit Graph

48 Commits

Author SHA1 Message Date
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
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
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
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
e7efe033be fix sessions 2021-10-30 11:11:24 +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
Claude Marche
c4366cb352 update sessions 2019-05-06 22:35:38 +02: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
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
Claude Marche
b8877c8063 replay obsolete sessions 2017-05-31 18:41:55 +02:00
Jean-Christophe Filliatre
1c16527133 updated proof sesssions 
a temporary file examples/TODO lists all examples whose
proof is yet to be updated
 2017-05-16 14:17:23 +02:00
Guillaume Melquiond
57d1a4be31 Merge branch 'master' into new_system 
Conflicts:
	Version
	doc/manual.tex
	examples/add_list/why3session.xml
	examples/algo63/why3session.xml
	examples/algo64/why3session.xml
	examples/algo65/why3session.xml
	examples/all_distinct/why3session.xml
	examples/arm/why3session.xml
	examples/assigning_meanings_to_programs/why3session.xml
	examples/binary_multiplication.mlw
	examples/binary_multiplication/why3session.xml
	examples/binary_multiplication/why3shapes.gz
	examples/binary_search/why3session.xml
	examples/binary_sqrt/why3session.xml
	examples/bitcount/why3session.xml
	examples/bitvector_examples/why3session.xml
	examples/bitwalker/why3session.xml
	examples/braun_trees/why3session.xml
	examples/bresenham/why3session.xml
	examples/bubble_sort/why3session.xml
	examples/coincidence_count/why3session.xml
	examples/conjugate/why3session.xml
	examples/counting_sort/why3session.xml
	examples/cursor/why3session.xml
	examples/cursor/why3shapes.gz
	examples/defunctionalization/why3session.xml
	examples/dfa_example/why3session.xml
	examples/dfs/why3session.xml
	examples/fibonacci/why3session.xml
	examples/finite_tarski/why3session.xml
	examples/flag2/why3session.xml
	examples/gcd/why3session.xml
	examples/gcd_bezout/why3session.xml
	examples/gcd_bezout/why3shapes.gz
	examples/hackers-delight/why3session.xml
	examples/linked_list_rev/why3session.xml
	examples/mccarthy.mlw
	examples/mccarthy/why3session.xml
	examples/mccarthy/why3shapes.gz
	examples/patience/why3session.xml
	examples/power/why3session.xml
	examples/power/why3shapes.gz
	examples/queens_bv/why3session.xml
	examples/register_allocation/why3session.xml
	examples/schorr_waite/why3session.xml
	examples/schorr_waite/why3shapes.gz
	examples/sudoku/why3session.xml
	examples/verifythis_fm2012_treedel/why3session.xml
	modules/array.mlw
	share/emacs/why3.el
	share/latex/why3lang.sty
	src/core/pretty.ml
	src/core/task.mli
	src/driver/autodetection.ml
	src/printer/alt_ergo.ml
	src/tools/why3prove.ml
	src/transform/eval_match.ml
	src/transform/prepare_for_counterexmp.ml
	src/transform/split_goal.ml
	src/util/strings.mli
	src/why3session/why3session_html.ml
 2016-06-16 08:23:43 +02:00