Commits · 1cd3800fe8d5a6d6259d3d8f8462ea2798de017b · Why3 / why3

06 Jan, 2015 7 commits
- Z3 4.3.2 is not obsolete (there is no stable 4.3.3 yet) · 1cd3800f
  MARCHE Claude authored Jan 06, 2015
  
  1cd3800f
- make cos, sin, tan, atan and pi built-in symbols for SMTv2 · 866daead
  MARCHE Claude authored Jan 06, 2015
```
Z3 apparently supports them, but any attempt to use thme makes Z3 segfault
```
  866daead
- Improve error recovery of why3doc in case of ill-formed comments. · 81e4e058
  Guillaume Melquiond authored Jan 06, 2015
  
  81e4e058
- nightly bench: allow coq8.4pl5 as an alternative to pl4 · 2d874522
  MARCHE Claude authored Jan 06, 2015
  
  2d874522
- upgraded proofs · 0748bb0f
  MARCHE Claude authored Jan 06, 2015
  
  0748bb0f
- Support for Alt-Ergo 1.00~beta (academia only) · c11e26d5
  MARCHE Claude authored Jan 06, 2015
```
detect it with

why3 config --add-prover alt-ergo /usr/local/bin/alt-ergo-1.00~beta.prv
```
  c11e26d5
- support for Alt-Ergo 0.99.1 · 5030e3ae
  MARCHE Claude authored Jan 06, 2015
  
  5030e3ae
05 Jan, 2015 4 commits
- Ity: eff_write takes a set of fields · 9df8c727
  Andrei Paskevich authored Jan 05, 2015
  
  9df8c727
- Expr: letrecs without variants are divergent · 5bd30629
  Andrei Paskevich authored Jan 05, 2015
  
  5bd30629
- Printer coq: fix missing parenthesis · d7c34bb5
  Martin Clochard authored Jan 05, 2015
  
  d7c34bb5
- parser: was rejected by last version of Menhir · c5b83d2a
  Martin Clochard authored Jan 05, 2015
  
  c5b83d2a
02 Jan, 2015 1 commit
- OCaml driver for peano.Peano: fixed a typo · 03bcdcbb
  Jean-Christophe Filliâtre authored Jan 02, 2015
  
  03bcdcbb
21 Dec, 2014 3 commits
- Expr: forbid PKls, store the mfield pv inside psymbols · 46bac1d0
  Andrei Paskevich authored Dec 21, 2014
```
Dexpr: more stuff
```
  46bac1d0
- updated sessions with Alt-ergo 0.95.2 · 0a24262b
  MARCHE Claude authored Dec 21, 2014
  
  0a24262b
- Expr: built-in symbols · 596bf275
  Andrei Paskevich authored Dec 21, 2014
  
  596bf275
19 Dec, 2014 5 commits
- Dexpr: more · f95f8bdd
  Andrei Paskevich authored Dec 19, 2014
  
  f95f8bdd
- Dexpr: minor · dacdfe37
  Andrei Paskevich authored Dec 19, 2014
  
  dacdfe37
- ide: display warnings after reload (and limit their number) · b454f245
  MARCHE Claude authored Dec 19, 2014
  
  b454f245
- removal of timelimit when step limit is present · dd5ffa4e
  Clément Fumex authored Dec 19, 2014
  
  dd5ffa4e
- Dexpr: destructive type unification · c786f7b9
  Andrei Paskevich authored Dec 19, 2014
  
  c786f7b9
18 Dec, 2014 1 commit
- support for coq 8.4pl5 · 1ff46ebe
  MARCHE Claude authored Dec 18, 2014
  
  1ff46ebe
12 Dec, 2014 2 commits
- fix a comment · 9e1326ec
  MARCHE Claude authored Dec 12, 2014
  
  9e1326ec
- (Work in progress) formalization of why3 logic · 4b810a5b
  Martin Clochard authored Dec 12, 2014
  
  4b810a5b
11 Dec, 2014 1 commit
- Expr: store the "decrease" predicate symbol inside rec_defn · dc9cfb96
  Andrei Paskevich authored Dec 11, 2014
  
  dc9cfb96
10 Dec, 2014 1 commit
- Expr: recursive funciton definitions (tbc) · fe7ab6b7
  Andrei Paskevich authored Dec 11, 2014
  
  fe7ab6b7
09 Dec, 2014 1 commit
- eliminate_epsilon: uniform handling of partial applications · f5cca463
  Martin Clochard authored Dec 09, 2014
  
  f5cca463
08 Dec, 2014 1 commit
- Ity: handle cty-to-mapping type casts in cty_apply · 64506ccb
  Andrei Paskevich authored Dec 08, 2014
```
Expr: create_rec_defn (wip)
```
  64506ccb
06 Dec, 2014 1 commit
- do not rebuild isabelle heap at each run of make · 831ceb0f
  MARCHE Claude authored Dec 06, 2014
  
  831ceb0f
05 Dec, 2014 4 commits
- z3 > 4.3.1 don't have a specific logic set, it will choose by itself · 273f4bde
  Clément Fumex authored Dec 05, 2014
  
  273f4bde
- minor modification in the nightly-bench script · 41ea4230
  Andrei Paskevich authored Dec 05, 2014
  
  41ea4230
- session update · 56c7eb03
  Clément Fumex authored Dec 05, 2014
  
  56c7eb03
- double-wp: fix missing proof. · f9c428af
  Martin Clochard authored Dec 05, 2014
  
  f9c428af
04 Dec, 2014 3 commits
- provers-detection-data.conf: mark old versions · 6c8e054b
  Andrei Paskevich authored Dec 04, 2014
  
  6c8e054b
- add support for Z3 4.3.3 · 8639ada5
  Andrei Paskevich authored Dec 04, 2014
  
  8639ada5
- z3_bare.drv: re-add "(set-logic AUFNIRA)" to the prelude · 8600e65a
  Andrei Paskevich authored Dec 04, 2014
  
  8600e65a
03 Dec, 2014 2 commits
- example hacker continued · 700f4deb
  Clément Fumex authored Dec 03, 2014
  
  700f4deb
- Driver smt-libv2 factorisé (pour cvc4 et z3) · f1c55bac
  Clément Fumex authored Dec 03, 2014
```
Module bitvec
```
  f1c55bac
02 Dec, 2014 1 commit
- Peano and one-time integers, with suitable drivers for OCaml extraction · 6d215c15
  Jean-Christophe Filliâtre authored Dec 02, 2014
  
  6d215c15
29 Nov, 2014 2 commits
- drivers: empty theories and modules are allowed · dbf8fc7d
  Jean-Christophe Filliâtre authored Nov 29, 2014
  
  dbf8fc7d
- why3extract: specifying more than one driver is an error · 00b0d570
  Jean-Christophe Filliâtre authored Nov 29, 2014
  
  00b0d570