| Merge branch 'ocaml5' into 'master' |
|
More...
|
almost 3 years ago
|
| Add meta compute_max_steps in rac.mlw to avoid warnings |
|
More...
|
almost 3 years ago
|
| Compute max size once for all / Reactivate warning |
|
More...
|
almost 3 years ago
|
| Fix compilation warnings |
|
More...
|
almost 3 years ago
|
| Check for absence of overflow when computing term size |
|
More...
|
almost 3 years ago
|
| Support for decimals and fractions as real values |
|
More...
|
almost 3 years ago
|
| bench/check-ce: fix steps for CVC5 after renaming of maps into maps_poly |
|
More...
|
almost 3 years ago
|
| Merge branch 'add-mono-versions-ce-bench' into 'master' |
|
More...
|
almost 3 years ago
|
| Merge branch 'yet-yet-another-list-reversal' into 'master' |
|
More...
|
almost 3 years ago
|
| Merge branch 'master' into yet-yet-another-list-reversal |
|
More...
|
almost 3 years ago
|
| gallery: list reversal terminates, even on cyclic lists |
|
More...
|
almost 3 years ago
|
| Add support for Alt-Ergo 2.4.2 (release August 1st 2022) |
|
More...
|
almost 3 years ago
|
| fix prover name in session for Alt-Ergo FPA |
|
More...
|
almost 3 years ago
|
| simplify computation of term size. Detailed warning message |
|
More...
|
almost 3 years ago
|
| Merge branch 'master' into 703-term-size-explosion-in-reduction-engine |
|
More...
|
almost 3 years ago
|
| Fix setting for Alt-Ergo-fpa |
|
More...
|
almost 3 years ago
|
| Merged master |
|
More...
|
almost 3 years ago
|
| Turn def of max_int, max_real into lemmas, fix bench-ce oracles |
|
More...
|
almost 3 years ago
|
| Merge branch '438-add-floating-point-support-by-alt-ergo-fpa-and-mathsat' into 'master' |
|
More...
|
almost 3 years ago
|
| Add an alternative "FPA" to Alt-Ergo, supporting dedicated reasoning on floating-point and real numbers |
|
More...
|
almost 3 years ago
|
| Merge branch 'master' into dreal |
|
More...
|
almost 3 years ago
|
| Merge branch 'emacs-locations' into 'master' |
|
More...
|
almost 3 years ago
|
| Explain to Emacs how Why3 locate errors. |
|
More...
|
almost 3 years ago
|
| Minor code cleanup |
|
More...
|
almost 3 years ago
|
| Improve parsing of prover variables |
|
More...
|
almost 3 years ago
|
| Cleanup obsolete code |
|
More...
|
almost 3 years ago
|
| [driver] exposes call-on-buffer from driver |
|
More...
|
almost 3 years ago
|
| Import a constructor value in RAC if the epsilon term is of a specific pattern |
|
More...
|
almost 3 years ago
|
| Add monomorphic versions for tests with polymorphism in CE bench |
|
More...
|
almost 3 years ago
|
| Updated realizations |
|
More...
|
almost 3 years ago
|
