Public Git Hosting - why3.git/search

2024-11-14	MARCHE Claude	Merge branch 'extensional' into 'master'	commit \| commitdiff \| tree
2024-11-14	Claude Marche	fix sessions and CE oracles	commit \| commitdiff \| tree
2024-11-13	Claude Marche	fix realizations	commit \| commitdiff \| tree
2024-11-13	Claude Marche	two forms of transformation extensionality	commit \| commitdiff \| tree
2024-11-13	Claude Marche	add regression test from BTS	commit \| commitdiff \| tree
2024-11-08	MARCHE Claude	Merge branch 'fmap_additional_operators' into 'master'	commit \| commitdiff \| tree
2024-11-08	Claude Marche	Additional operators for fmaps	commit \| commitdiff \| tree
2024-11-04	MARCHE Claude	Merge branch 'fix-example-rightmost-bit-trick' into...	commit \| commitdiff \| tree
2024-11-04	Claude Marche	remove use of cvc5 1.2.0	commit \| commitdiff \| tree
2024-11-03	MARCHE Claude	Merge branch 'improved-proof-of-rightmostbittrick'...	commit \| commitdiff \| tree
2024-11-03	MARCHE Claude	Merge branch '585-new-function-for-conversion-from...	commit \| commitdiff \| tree
2024-11-03	MARCHE Claude	Adding a function `from_real` in the theory of IEEE...	commit \| commitdiff \| tree
2024-11-03	Claude Marche	improved proof	commit \| commitdiff \| tree
2024-11-03	MARCHE Claude	Merge branch 'bench_add_category_java_extract' into...	commit \| commitdiff \| tree
2024-11-03	Claude Marche	add category for java extraction	commit \| commitdiff \| tree
2024-11-03	Claude Marche	update sessions	commit \| commitdiff \| tree
2024-11-02	MARCHE Claude	Merge branch '637-provide-axioms-for-sdiv-and-smod...	commit \| commitdiff \| tree
2024-11-02	MARCHE Claude	Resolve "provide axioms for sdiv and smod in theory...	commit \| commitdiff \| tree
2024-10-31	MARCHE Claude	Merge branch 'strengthen-use-of-partial-keyword' into...	commit \| commitdiff \| tree
2024-10-31	MARCHE Claude	do not allow implicit inference of partial	commit \| commitdiff \| tree
2024-10-31	MARCHE Claude	Merge branch '616-extend-ptree-helpers' into 'master'	commit \| commitdiff \| tree
2024-10-30	Claude Marche	improved Ptree helpers	commit \| commitdiff \| tree
2024-10-29	MARCHE Claude	Merge branch 'remove-unused-dep-for-sequences' into...	commit \| commitdiff \| tree
2024-10-29	MARCHE Claude	add metas for unused-dependencies on sequences	commit \| commitdiff \| tree
2024-10-27	MARCHE Claude	Merge branch 'fix_obsolete' into 'master'	commit \| commitdiff \| tree
2024-10-27	Claude Marche	fix obsolete sessions	commit \| commitdiff \| tree
2024-10-25	MARCHE Claude	Merge branch 'unused_dependencies_in_generated_axioms...	commit \| commitdiff \| tree
2024-10-25	MARCHE Claude	Add metas for unused dependencies in generated axioms	commit \| commitdiff \| tree
2024-10-25	MARCHE Claude	Merge branch '581-mlw-printer-incorrect-for-eoptexn...	commit \| commitdiff \| tree
2024-10-25	Claude Marche	Improve Mlw_printer for Eoptexn	commit \| commitdiff \| tree
2024-10-23	MARCHE Claude	Merge branch 'unused_dep_for_euclidean_div_mod' into...	commit \| commitdiff \| tree
2024-10-23	MARCHE Claude	unused dependencies on Euclidean div/mod	commit \| commitdiff \| tree
2024-10-22	MARCHE Claude	Merge branch 'unused_dep_for_bvlib' into 'master'	commit \| commitdiff \| tree
2024-10-22	MARCHE Claude	fix closure computation in `remove_unused`	commit \| commitdiff \| tree
2024-10-22	MARCHE Claude	Merge branch 'model-from-rac-log' into 'master'	commit \| commitdiff \| tree
2024-10-22	Claude Marche	oracles update	commit \| commitdiff \| tree
2024-10-21	Claude Marche	remove unused files, refine statistics	commit \| commitdiff \| tree
2024-10-21	Claude Marche	oracle changes OK	commit \| commitdiff \| tree
2024-10-18	MARCHE Claude	Merge branch 'extend-why3-pp-latex' into 'master'	commit \| commitdiff \| tree
2024-10-18	Claude Marche	also output type definitions and logic definitions	commit \| commitdiff \| tree
2024-10-12	MARCHE Claude	Merge branch '878-span-file-resolution-logic-different...	commit \| commitdiff \| tree
2024-10-12	Claude Marche	make span file names relative to the file they appear...	commit \| commitdiff \| tree
2024-10-12	MARCHE Claude	Merge branch 'fix_ce_bench' into 'master'	commit \| commitdiff \| tree
2024-10-12	MARCHE Claude	ensure step limit has priority over time limit	commit \| commitdiff \| tree
2024-10-11	MARCHE Claude	Merge branch '847-evaluate-impact-of-intro-vc-vars...	commit \| commitdiff \| tree
2024-10-11	MARCHE Claude	Merge branch 'ensures_filenames_in_spans_are_relative_to_the...	commit \| commitdiff \| tree
2024-10-11	MARCHE Claude	CFG typing: locate exceptions raised by use/import	commit \| commitdiff \| tree
2024-10-08	MARCHE Claude	Merge branch '877-rac-does-not-take-steplimit-into...	commit \| commitdiff \| tree
2024-10-08	MARCHE Claude	do not take resource limits from more than one source	commit \| commitdiff \| tree
2024-10-08	MARCHE Claude	Merge branch '881-alt-ergo-2-6-don-t-need-fpa-alternative...	commit \| commitdiff \| tree
2024-10-08	MARCHE Claude	drivers for Alt-Ergo 2.6: FPA implicit, CE and BV	commit \| commitdiff \| tree
2024-10-04	MARCHE Claude	Merge branch 'pow2int_bv' into 'master'	commit \| commitdiff \| tree
2024-10-03	MARCHE Claude	Merge branch '880-add-support-for-alt-ergo-2-6-and...	commit \| commitdiff \| tree
2024-10-03	MARCHE Claude	Merge branch 'support-for-coq-8.19.2' into 'master'	commit \| commitdiff \| tree
2024-10-03	Claude Marche	Support for Alt-Ergo 2.6.0	commit \| commitdiff \| tree
2024-10-03	Claude Marche	Support for Coq 8.19.2	commit \| commitdiff \| tree
2024-10-03	Claude Marche	Support for Z3 4.13 and cvc5 1.1 and 1.2	commit \| commitdiff \| tree
2024-10-02	MARCHE Claude	Merge branch 'c_extraction_global_variables' into ...	commit \| commitdiff \| tree
2024-10-02	MARCHE Claude	extraction to C: extract global variables	commit \| commitdiff \| tree
2024-10-02	MARCHE Claude	Fix doc of extraction to C for records with mutable...	commit \| commitdiff \| tree
2024-10-01	MARCHE Claude	Merge branch 'remove_unneeded_ghost_qualifier' into...	commit \| commitdiff \| tree
2024-10-01	MARCHE Claude	clarify ghost and non-ghost for reals and ufloats	commit \| commitdiff \| tree
2024-10-01	MARCHE Claude	Merge branch '842-why3-execute-type-inference-problem...	commit \| commitdiff \| tree
2024-10-01	MARCHE Claude	take type variables instances into account in execution...	commit \| commitdiff \| tree
2024-09-26	MARCHE Claude	Merge branch '876-ide-crashes-when-clicking-on-goal...	commit \| commitdiff \| tree
2024-09-26	Claude Marche	do not fail when goal as no loc when stack_trace is...	commit \| commitdiff \| tree
2024-09-26	MARCHE Claude	Merge branch 'example-r-cos-theta' into 'master'	commit \| commitdiff \| tree
2024-09-24	Claude Marche	new example for numeric strategy	commit \| commitdiff \| tree
2024-09-20	MARCHE Claude	Merge branch 'rac-incomplete-better-trace' into 'master'	commit \| commitdiff \| tree
2024-09-19	MARCHE Claude	Merge branch '306-add-program-equality-on-boolean-type...	commit \| commitdiff \| tree
2024-09-19	MARCHE Claude	Pmodule: t->t->t functions can be overloaded as X-...	commit \| commitdiff \| tree
2024-09-19	MARCHE Claude	Merge branch '638-fix-usage-of-optional-argument-me_name_tra...	commit \| commitdiff \| tree
2024-09-19	MARCHE Claude	get rid of print_model_human and the filter_similar...	commit \| commitdiff \| tree
2024-09-18	MARCHE Claude	Merge branch 'fix_missing_edited_files' into 'master'	commit \| commitdiff \| tree
2024-09-18	Claude Marche	fix session having extra edited files	commit \| commitdiff \| tree
2024-09-18	MARCHE Claude	Merge branch '848-get-rid-of-option-json-values-in...	commit \| commitdiff \| tree
2024-09-17	MARCHE Claude	Merge branch 'bvconverter256' into 'master'	commit \| commitdiff \| tree
2024-09-17	MARCHE Claude	Merge branch '855-driver-alt-ergo-fpa-should-not-use...	commit \| commitdiff \| tree
2024-09-17	MARCHE Claude	check that `real.FromInt.from_int` is correctly sent...	commit \| commitdiff \| tree
2024-09-16	MARCHE Claude	Merge branch '870-call_provers-analyze_result-defaults...	commit \| commitdiff \| tree
2024-09-13	MARCHE Claude	Merge branch 'document-extraction-to-C' into 'master'	commit \| commitdiff \| tree
2024-09-13	Claude Marche	Augment documentation of extraction to C	commit \| commitdiff \| tree
2024-09-03	MARCHE Claude	Merge branch 'list-length-via-peano' into 'master'	commit \| commitdiff \| tree
2024-09-03	MARCHE Claude	List length via peano	commit \| commitdiff \| tree
2024-09-02	MARCHE Claude	Merge branch 'list-length-as-int63' into 'master'	commit \| commitdiff \| tree
2024-09-02	MARCHE Claude	Merge branch 'proofs-without-fpa' into 'master'	commit \| commitdiff \| tree
2024-09-02	Claude Marche	compute a list length as a 63-bit integer	commit \| commitdiff \| tree
2024-09-02	Claude Marche	no need for FPa for these proofs	commit \| commitdiff \| tree
2024-07-11	MARCHE Claude	Merge branch 'rac-incomplete-better-trace' into 'master'	commit \| commitdiff \| tree
2024-07-05	MARCHE Claude	Merge branch '867-forward-propagation-strategy-bug...	commit \| commitdiff \| tree
2024-07-01	MARCHE Claude	Merge branch '866-why3-ide-exits-abruptly-when-a-language...	commit \| commitdiff \| tree
2024-07-01	Claude Marche	Do not exit abruptly when problem with lang occur	commit \| commitdiff \| tree
2024-06-24	MARCHE Claude	Merge branch '863-forward-propagation-strategy-accept...	commit \| commitdiff \| tree
2024-06-21	MARCHE Claude	Merge branch 'fix_proofs_with_coq_8_19' into 'master'	commit \| commitdiff \| tree
2024-06-21	MARCHE Claude	Merge branch 'improve_numeric_examples_on_sin_cos'...	commit \| commitdiff \| tree
2024-06-21	Claude Marche	fix proofs, including one failing with Coq 8.19	commit \| commitdiff \| tree
2024-06-21	Claude Marche	improve readibility, and various small improvements	commit \| commitdiff \| tree
2024-06-21	MARCHE Claude	Merge branch '838-problem-with-instantiation-of-interfaces...	commit \| commitdiff \| tree
2024-06-20	MARCHE Claude	Merge branch 'cleaning_again_example_sin_cos' into...	commit \| commitdiff \| tree
2024-06-20	MARCHE Claude	Merge branch '845-why3-does-not-support-coq-8-19' into...	commit \| commitdiff \| tree
next

A platform for deductive program verification

RSS Atom