Internal error in Alt-ergo after inline_trivial
Alt-ergo fails on the VC for x
in the example below after applying the transformation inline_trivial
:
Example:
use int.Int
use mach.int.Int32
lemma x: 0 < 1
Alt-ergo output:
internal failure: Ident (>) is not yet declared
Any ideas where this comes might come from? Too much inlining (losing the definition of >
) or too little (retaining the use of >
)? Removing the second line does not change the VC to my understanding but make the error disappear…
(Why3 from last Monday (8f9a5016) and Alt-ergo 2.2.0/2.3.0)