Iterated-induction file has extra code

[Former user]

if isinvariant(T,invariant) then
    print("----> Okay, we proved --using the induction method-- that in every context, our invariant is satisfied")
else
    print("----> Prover could not prove the invariant")
end

is repeated. This causes a failure.

[Bart Bogaerts]

Hi,

This code is not actually repeated. It is executed once with a structure (checking if it's a finite domain invariant) and once without S, using a theorem prover to prove invariance.

What kind of failure are you experiencing exactly?

A crash? Or the prover failing to prove the invariant?

[Bart Bogaerts]

Addition: in the last released version (3.3.0) some parts of the translation of the call to the theorem prover were not yet implemented, Thus, possibly causing

Error: Entailment checking is not supported for the provided theories.

In the development, this is already fixed...