alt-ergo

alt-ergo copied to clipboard

ACoquereau

The following formula is unsat: ``` (declare-fun s () Int) (declare-fun y () Int) (declare-fun th () Int) (assert (> s 0)) (assert (>= s (+ (* y s) 1)))...

iguerNL

[Documentation] have doc for each version

1

doc versions: - 2.3.2 - 2.4.0 - ... - dev

ACoquereau

[Build] add more checks

1

- Loading and running of plugins / parsers - Loading of preludes - Make rules (archi, ..) - Check if `--where` option results are correct

ACoquereau

See what has been done for Arithmetic's `add` here: https://github.com/OCamlPro/alt-ergo/pull/432/commits/c02878cb2758ae96a28e52a4fae6f1461ae1b15d

iguerNL

[Gui] move altgr-ergo.conf file in the share/alt-ergo directory of current opam switch

1

Add option to specify share directory in configure

ACoquereau

Currently, a let symbol is seen as a Var, and eliminated by introduction a skolem-like function.

iguerNL

Expressions purification

1

For the following example: ``` logic a, b, c : prop logic x, y, z : int logic f : 'a -> int goal g: let tmp = if (a...

iguerNL

Stdout used instead of stderr

1

- This behavior is noticed for models (which can be on stdout in the default setting, but we should be able to select a different std) - The behavior is...

iguerNL

See the comment at the end of the ac.ml file for more details

iguerNL