alt-ergo

alt-ergo copied to clipboard

**Example 1:** ``` type t logic a : t logic P : 'a -> prop goal g: P(1) -> P(2.5) -> P(true) -> P(a) -> false ``` AE outputs: ```...

iguerNL

Invalid_argument("List.fold_left2") when trying to get a model

2

command: ``` ./alt-ergo tables-Map-VC_add_max_binding.ae --interpretation last --timelimit 1 --output smtlib2 --timelimit-interpretation 1 ``` File: [bug.ae.zip](https://github.com/OCamlPro/alt-ergo/files/5803877/bug.ae.zip) Output: ``` ; Functions (define-fun key ((arg_0 (t1, '_c0) tuple2)) t1 k0) (define-fun key ((arg_0...

iguerNL

Alt-Ergo fails to type-check the following example: ``` type 'a s = A of { sel_A1 : int ; sel_A2 : int } | B of { sel_B1 : int...

iguerNL

iguerNL

incremental mode vs multi-goals: currently, work is done twice

1

Once https://github.com/OCamlPro/alt-ergo/pull/371 is merged, Alt-Ergo will support SMT2 incremental mode (push/pop). But the way things are done in - psmt2_to_alt_ergo (translates `check-sat` and `check-sat-assuming` commands to `goal`) - main_text (all...

iguerNL

If some soft uses alt-ergo-lib and maintains two instances of the lib's state, this is not correct.

iguerNL

Original question in review of https://github.com/OCamlPro/alt-ergo/pull/371 ``` Another question related to save/replay used-context: an extra work is probably needed. This is probably already done for native-lang's multi-goals feature, and we...

iguerNL

Related to PR: https://github.com/OCamlPro/alt-ergo/pull/371

iguerNL

iguerNL

opam package: make alt-ergo and alt-ergo-free uncompatible (whatever the version)

1

Currently, one can install latest versions of both alt-ergo and alt-ergo-free, which is bad, because both packages provide a binary called `alt-ergo`.

iguerNL