alt-ergo
alt-ergo copied to clipboard
OCamlPro
OCamlPro public development repository for Alt-Ergo
Alt-ergo seems to enter an infinite loop on the following example: ``` type 'a t = Cons of {elt : 'a; tail : 'a t} | Nil function length (list...
Changing the installation section for plugins and preludes from `share` to `lib` (to fix issues #504 and #509). If some users use the plugins and look for them in `/usr/share`...
This PR consists in replacing the old bash scripts used for running the non-regression tests by a mighty Ocaml script. I moved most of the tests from `/non-regression` directory to...
This PR removes most of the global opens in the Alt-Ergo library. They are replaced by local opens, aliases and explicit type annotations.
This PR implements the model generation for ADT. The model generation is done by the casesplit mechanism in `Adt_rel`. - If `--enable-adts-cs` is present, we do casesplits by choosing a...
Consider the following program. ```ocaml let () = Options.set_debug_explanations true; Options.set_verbose true; let fresh q = Ex.singleton @@ Ex.Dep (Expr.mk_term (Sy.Real q) [] Tbool) in let interval lo hi =...
This patch adds interval domains to the Bitv_rel module, as well as interreductions between the bitlist and interval domains following: Sharpening Constraint Programming approaches for Bit-Vector Theory. Zakaria Chihani, Bruno...
This PR is rebased on #1078 and #1086.