GitLab

the verification algorithm must always terminate and be reasonably
performant in practice, but its worst-case complexity is unknown
and probably exponential. What is quite easy when there is only
one recursive definition, becomes difficult when there is a group
of mutually recursive definitions. An educated discussion would
be highly appreciated.

BTW, I had to convert a couple of recursive "logic"s on integers
into an abstract "logic" + axiom. Pretty much all of them supposed
that the argument was non-negative, and thus were non-terminating!

programs: as a side-effect of the new for loop, the syntax 'variant {t} for R' is changed into 'variant {t} with R' (no big deal, it is rarely used)

if the extension or the format is not recognised

  in the logic language into (more or less) higher-order style.
  For example,

    logic func (x : int, y : int, 'a list) : (int, 'a) map list

    logic pred (bool, int * real)

  is now written:
    
    logic func (x y : int) (list 'a) : list (map int 'a)

    logic pred bool (int, real)

  Note that types use prefix notation (as in Coq) and the types
  of tuples are now written as (type1, type2, ..., typeN).

- Use the same syntax of type expressions in the program language.

- Allow binders of the form (x y:int) in the program language.
  

bench : ajout d'un bench pour tester tous les provers sur des buts triviaux. Cela peut permettre de détecter un mauvais driver ou printer.

programs: WP for exceptions
why.conf: removed -debug flag for alt-ergo