Commits · 8a6f61edb17cd74f06e4eb22084913afc54324ee · Why3 / why3

15 Mar, 2016 3 commits
- Fix typo. · 8a6f61ed
  Guillaume Melquiond authored Mar 15, 2016
  
  8a6f61ed
- headers 2016 · 0cc11b0c
  Andrei Paskevich authored Mar 15, 2016
  
  0cc11b0c
- Do not set a wallclock time limit if there is no time limit. · b8997b1a
  Guillaume Melquiond authored Mar 15, 2016
  
  b8997b1a
14 Mar, 2016 2 commits
- Session: fix a typo · ca7e7cd7
  Andrei Paskevich authored Mar 14, 2016
  
  ca7e7cd7
- driver Z3 4.3.2: should not use native BV theory at all · 3327989e
  MARCHE Claude authored Mar 14, 2016
  
  3327989e
11 Mar, 2016 3 commits
- Remove files for boomy and jstree from repository. · 52d9e192
  Guillaume Melquiond authored Mar 11, 2016
  
  52d9e192
- Remove the "jstree" style from "session". · 4f150358
  Guillaume Melquiond authored Mar 11, 2016
  
  4f150358
- do not publicize the SafeProver · 06285130
  MARCHE Claude authored Mar 11, 2016
  
  06285130
09 Mar, 2016 1 commit
- Fixed bug introduced by the groupment of limits · dac73b72
  MARCHE Claude authored Mar 09, 2016
  
  dac73b72
08 Mar, 2016 3 commits
- follow up fix of why3tac · ee430035
  Johannes Kanig authored Mar 09, 2016
  
  ee430035
- group all limits into a single object · 643936c5
  Johannes Kanig authored Mar 09, 2016
```
makes API of Call_provers and Driver a bit simpler
```
  643936c5
- addressing FIXME comments in code · a164de08
  Johannes Kanig authored Mar 08, 2016
  
  a164de08
07 Mar, 2016 3 commits
- example gcd_bezout: additional assert to help provers · bd4383b4
  MARCHE Claude authored Mar 07, 2016
  
  bd4383b4
- example isqrt: additional lemmas and assert to ease the proofs · 588edddb
  MARCHE Claude authored Mar 07, 2016
  
  588edddb
- examples(wip): 2wp_gen · da34dca3
  Martin Clochard authored Mar 07, 2016
  
  da34dca3
26 Feb, 2016 4 commits
- Support for Z3 4.4.1, Alt-Ergo 1.20.prv · 2411344a
  MARCHE Claude authored Feb 26, 2016
  
  2411344a
- provers-detection: Alt-Ergo 1.01 · 56702947
  Andrei Paskevich authored Feb 26, 2016
  
  56702947
- new example: patience game (VSTTE 14) · 7557425f
  MARCHE Claude authored Feb 26, 2016
  
  7557425f
- example tree reconstruction: remove a few Coq proofs · b12acb40
  MARCHE Claude authored Feb 26, 2016
  
  b12acb40
25 Feb, 2016 2 commits
- Prevent anomaly on accessing the missing body of opaque constants in the Coq tactic. · ae62fcce
  Guillaume Melquiond authored Feb 25, 2016
  
  ae62fcce
- Lazily load references to constants inside the Coq tactic. · 90958d5d
  Guillaume Melquiond authored Feb 25, 2016
  
  90958d5d
24 Feb, 2016 8 commits
- install: fix case of non-free iconsets · 6b4e99f7
  MARCHE Claude authored Feb 24, 2016
  
  6b4e99f7
- sessions replayed on moloch · 3a58b910
  MARCHE Claude authored Feb 24, 2016
  
  3a58b910
- Revert "sessions replayed on moloch" · 4383d9c8
  MARCHE Claude authored Feb 24, 2016
```
This reverts commit 838ed39a.
```
  4383d9c8
- sessions replayed on moloch · 838ed39a
  MARCHE Claude authored Feb 24, 2016
  
  838ed39a
- Sessions: last updates for coq 8.5 · 8f96c0ed
  MARCHE Claude authored Feb 24, 2016
  
  8f96c0ed
- small fix on session · 25554264
  MARCHE Claude authored Feb 24, 2016
  
  25554264
- Sessions: updated on moloch · 26a47423
  MARCHE Claude authored Feb 24, 2016
  
  26a47423
- Isabelle realizations: update for removed axioms from BV theories · e2b5e272
  MARCHE Claude authored Feb 24, 2016
  
  e2b5e272
23 Feb, 2016 7 commits
- sessions: more updates for Coq 8.5 · 701397eb
  MARCHE Claude authored Feb 23, 2016
  
  701397eb
- remove unecessary axioms from bv theory clones and consequently fix examples · 6c985576
  Clément Fumex authored Feb 23, 2016
  
  6c985576
- sessions: more updates for Coq 8.5 · 98920324
  MARCHE Claude authored Feb 23, 2016
  
  98920324
- BV realisation: ignore file · 5a24300d
  MARCHE Claude authored Feb 23, 2016
  
  5a24300d
- nightly bench: replay proofs with coq 8.5 using Coq 8.4pl6 · 0e378e25
  MARCHE Claude authored Feb 23, 2016
  
  0e378e25
- sessions: more updates with Coq 8.5 · 7e94fa68
  MARCHE Claude authored Feb 23, 2016
  
  7e94fa68
- sessions: some updates for compatibility with Coq 8.5 · 34c5aeb6
  MARCHE Claude authored Feb 23, 2016
  
  34c5aeb6
22 Feb, 2016 4 commits
- Coq tactic: works with Coq 8.5 · 86a95cbe
  MARCHE Claude authored Feb 22, 2016
```
also compatible with Coq 8.4
```
  86a95cbe
- examples/in_progress: 2wp_gen, makefile · a36ddc02
  Martin Clochard authored Feb 22, 2016
  
  a36ddc02
- examples/in_progress: 2wp_gen, cont'd · 15d07791
  Martin Clochard authored Feb 22, 2016
  
  15d07791
- BV theory: reverted removal of normally useless axiom · 58f09fef
  MARCHE Claude authored Feb 22, 2016
  
  58f09fef