- 22 Nov, 2017 2 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
-
- 06 Nov, 2017 1 commit
-
-
- 31 Oct, 2017 1 commit
-
-
MARCHE Claude authored
-
- 09 Sep, 2016 1 commit
-
-
Sylvain Dailler authored
Adding "I don't know" as a correct keyword for provers return (inside counterexamples). Updating scripts because of move from hoare_logic to WP_revisited. * src/driver/parse_smtv2_model.ml (parse): Adding I dont know as a keyword. * bench/bench Changing to WP_revisited. * examples/bench.sh Changing to WP_revisited. * examples/regtests.sh Changing to WP_revisited.
-
- 12 Feb, 2015 1 commit
-
-
MARCHE Claude authored
-
- 10 Sep, 2014 1 commit
-
-
MARCHE Claude authored
-
- 31 Aug, 2014 2 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
-
- 21 Aug, 2014 1 commit
-
-
Guillaume Melquiond authored
-
- 02 Jun, 2014 1 commit
-
-
Guillaume Melquiond authored
-
- 28 May, 2014 1 commit
-
-
Guillaume Melquiond authored
-
- 11 Mar, 2014 1 commit
-
-
Jean-Christophe Filliâtre authored
-
- 09 Mar, 2014 1 commit
-
-
Jean-Christophe Filliâtre authored
-
- 04 Mar, 2014 2 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
-
- 27 Feb, 2014 1 commit
-
-
Jean-Christophe Filliâtre authored
support for 31/32/63/64-bit integers in extracted code
-
- 25 Feb, 2014 1 commit
-
-
Jean-Christophe Filliâtre authored
-
- 21 Feb, 2014 2 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
-
- 16 Feb, 2014 1 commit
-
-
MARCHE Claude authored
-
- 15 Feb, 2014 2 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
-
- 14 Feb, 2014 1 commit
-
-
MARCHE Claude authored
-
- 03 Feb, 2014 4 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
- 28 Jan, 2014 1 commit
-
-
MARCHE Claude authored
-
- 21 Jan, 2014 1 commit
-
-
MARCHE Claude authored
-
- 16 Jan, 2014 2 commits
-
-
Jean-Christophe Filliâtre authored
-
MARCHE Claude authored
-
- 15 Jan, 2014 2 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
-
- 14 Jan, 2014 2 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
-
- 23 Mar, 2013 1 commit
-
-
Andrei Paskevich authored
they now live in examples/tests/ also, simplify bench/bench script
-
- 03 Feb, 2013 1 commit
-
-
Andrei Paskevich authored
-
- 30 Jan, 2013 2 commits
-
-
Andrei Paskevich authored
-
Andrei Paskevich authored
- all programs with sessions are in examples/ - all programs without sessions are in examples/in_progress/ (if you have private sessions for those, just move them there) - all pure logical problems are in logic/ (to simplify bench scripts and gallery building; they are few anyway) - all OCaml programs are in examples/use_api/ - all strange stuff is in examples/misc/ (most of it should probably go) - Claude's solutions for Foveoos 2011 are in examples/foveoos11-cm/ (why do we need two sets of solutions for quite simple problems?) - hoare_logic, bitvectors, vacid_0_binary_heaps are in examples/ Bench scripts and documentation are updated. Also, bench/bench is simplified a little bit.
-