Public Git Hosting - why3.git/commit

summary | log | graphiclog1 | graphiclog2 | commit | commitdiff | tree | refs | edit | fork
(parent: 1ed0f44) | patch

commit	0b76901deb1238f5933786085ed5627e228466ed
author	MARCHE Claude <claude.marche@inria.fr>
	Tue, 28 May 2024 13:10:42 +0000 (28 15:10 +0200)
committer	MARCHE Claude <claude.marche@inria.fr>
	Tue, 28 May 2024 13:10:42 +0000 (28 15:10 +0200)
tree	15c9d3fdc23c369e8d10e7a95f29f1c546cc2414	tree \| snapshot (tar.gz zip)
parent	1ed0f445a39b031c325b3aa3cd9d269a0292a6c2	commit \| diff

Reduce the size of the formula produced, using let bindings so as to share common subterms

17 files changed:

examples/numeric/add_sqrt/why3session.xml		diff \| blob \| blame \| history
examples/numeric/add_sqrt/why3shapes.gz		diff \| blob \| blame \| history
examples/numeric/add_sub_mul/why3session.xml		diff \| blob \| blame \| history
examples/numeric/add_sub_mul/why3shapes.gz		diff \| blob \| blame \| history
examples/numeric/addition/why3session.xml		diff \| blob \| blame \| history
examples/numeric/addition/why3shapes.gz		diff \| blob \| blame \| history
examples/numeric/exp_log/why3session.xml		diff \| blob \| blame \| history
examples/numeric/exp_log/why3shapes.gz		diff \| blob \| blame \| history
examples/numeric/multiplication.mlw		diff \| blob \| blame \| history
examples/numeric/multiplication/why3session.xml		diff \| blob \| blame \| history
examples/numeric/multiplication/why3shapes.gz		diff \| blob \| blame \| history
examples/numeric/sin_cos.mlw		diff \| blob \| blame \| history
examples/numeric/sin_cos/why3session.xml		diff \| blob \| blame \| history
examples/numeric/sin_cos/why3shapes.gz		diff \| blob \| blame \| history
examples/numeric/substraction/why3session.xml		diff \| blob \| blame \| history
examples/numeric/substraction/why3shapes.gz		diff \| blob \| blame \| history
plugins/strategies/forward_propagation.ml		diff \| blob \| blame \| history

A platform for deductive program verification