- 08 Dec, 2017 1 commit
-
-
MARCHE Claude authored
-
- 07 Dec, 2017 3 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
- 06 Dec, 2017 2 commits
-
-
MARCHE Claude authored
-
Sylvain Dailler authored
Also fix session for isqrt_von_neumann
-
- 05 Dec, 2017 8 commits
-
-
Sylvain Dailler authored
The factoring is recovered, the rest is not adapted.
-
Sylvain Dailler authored
The rest of this commit was discarded. It does not look to be adapted to the Why3 testsuite.
-
Sylvain Dailler authored
Could be simplified.
-
MARCHE Claude authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
MARCHE Claude authored
# Conflicts: # examples/bitvector_examples/why3session.xml # examples/bitvector_examples/why3shapes.gz
-
- 04 Dec, 2017 1 commit
-
-
MARCHE Claude authored
-
- 01 Dec, 2017 2 commits
-
-
MARCHE Claude authored
fix obsolete sessions
-
MARCHE Claude authored
-
- 30 Nov, 2017 4 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
-
Sylvain Dailler authored
The former realization of bv used a bit of sign as the less significant bit which should be the most significant. It did not raise problems because to_int and to_uint were not linked by an axiom in the .why. Now, it is the case, so we rewrote function twos_complement and made some straightforward changes to the existing realization (surprisingly proofs are the same).
-
MARCHE Claude authored
cleaning now removed all detached nodes below proved status is now computed ignoring detached nodes
-
- 29 Nov, 2017 12 commits
-
-
Guillaume Melquiond authored
This restores the gallery.
-
Guillaume Melquiond authored
-
Guillaume Melquiond authored
-
Guillaume Melquiond authored
-
Guillaume Melquiond authored
-
Guillaume Melquiond authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
MARCHE Claude authored
Merge branch 'spark_bitvector_theory_changes' of gitlab.inria.fr:why3/why3 into spark_bitvector_theory_changes
-
Sylvain Dailler authored
-
Sylvain Dailler authored
This reverts commit 2ff5ad5f.
-
- 28 Nov, 2017 3 commits
-
-
MARCHE Claude authored
replaced the 'variant {0}' by diverges to avoid unproved goals but now we have warnings. TO INVESTIGATE: uncomment the commented variants, that are supposed to work
-
MARCHE Claude authored
spaces in strategy names are not allowed anymore
-
MARCHE Claude authored
improve the startup sequence at the same time in particular, when source editing is disabled and there is a syntax or typing error, the GTK window does not 'blink' briefly before printing the error in the console
-
- 27 Nov, 2017 4 commits
-
-
Guillaume Melquiond authored
-
Guillaume Melquiond authored
Different symbols were assigned to constant zero, depnding on whether it was typed by the user or it was generated by Why3 in the variant-decrease verification condition, thus causing some TPTP provers to fail.
-
MARCHE Claude authored
-
MARCHE Claude authored
-