#8 Datatype Translation for Atelier-B throws IllegalArgumentException

[Son Hoang]

In the following attached project, invoking any Atelier-B provers on the remaining open sub-goal of the obligation thm1 will fails with "Internal error, see log file". The exception stack is as follow.

java.lang.IllegalArgumentException: Invalid type ℤ for expression op(p_p)
at org.eventb.internal.core.ast.FormulaChecks.ensureHasType(FormulaChecks.java:34)
at org.eventb.core.ast.ExtendedExpression.<init>(ExtendedExpression.java:205)
at org.eventb.core.ast.FormulaFactory.makeExtendedExpression(FormulaFactory.java:479)
at org.eventb.internal.core.ast.datatype.DatatypeRewriter.rewrite(DatatypeRewriter.java:121)
at org.eventb.core.ast.ExtendedExpression.rewrite(ExtendedExpression.java:427)
at org.eventb.core.ast.ExtendedExpression.rewrite(ExtendedExpression.java:1)
at org.eventb.core.ast.RelationalPredicate.rewrite(RelationalPredicate.java:407)
at org.eventb.core.ast.RelationalPredicate.rewrite(RelationalPredicate.java:1)
at org.eventb.core.ast.Formula.translateDatatype(Formula.java:2430)
at org.eventb.internal.core.seqprover.transformer.SequentDatatypeTranslator.transform(SequentDatatypeTranslator.java:38)
at org.eventb.internal.core.seqprover.transformer.TrackedPredicate.transform(TrackedPredicate.java:103)
at org.eventb.internal.core.seqprover.transformer.SimpleSequent.apply(SimpleSequent.java:115)
at org.eventb.core.seqprover.transformer.SimpleSequents.translateDatatypes(SimpleSequents.java:296)
at com.clearsy.atelierb.provers.internal.core.AtbProversCall.translateToClassicalB(AtbProversCall.java:186)
at com.clearsy.atelierb.provers.internal.core.AtbProversCall.run(AtbProversCall.java:214)
at java.util.concurrent.Executors$RunnableAdapter.call(Executors.java:471)
at java.util.concurrent.FutureTask.run(FutureTask.java:262)
at java.lang.Thread.run(Thread.java:745)

[Guillaume Verdier]

With the latest version of the plug-in, invoking Atelier-B provers on the goal works fine and doesn't throw any exception.