From 2a6afeffbacf1683acf57097223b13e381bd0d5a Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Tue, 24 Jun 2025 14:07:05 +0200
Subject: [PATCH] instanceof check before casting to IInvariant

for getting descriptions

Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>
---
 .../translator/internal/ModelTranslator.java  | 25 +++++++++++--------
 1 file changed, 15 insertions(+), 10 deletions(-)

diff --git a/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java b/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java
index beec5d95..094bac9f 100644
--- a/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java
+++ b/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java
@@ -580,16 +580,21 @@ public class ModelTranslator extends AbstractComponentTranslator {
 			if (isDefinedHere(evPredicate)) {
 				final PPredicate predicate = translatePredicate(ff, te,
 						evPredicate);
-				final IInvariant ucp = (IInvariant) evPredicate.getSource(); // comments only attached in unchecked source
-				if (ucp.hasAttribute(EventBAttributes.COMMENT_ATTRIBUTE)) {
-					final String commentString = ucp.getAttributeValue(EventBAttributes.COMMENT_ATTRIBUTE);
-					//System.out.println("Invariant/theorem " + predicate + " has description " + commentString);
-					final TPragmaFreeText desc = new TPragmaFreeText(commentString);
-					ADescriptionPragma descPragma = new ADescriptionPragma(Collections.singletonList(desc));
-					ADescriptionPredicate dpred = new ADescriptionPredicate(descPragma, predicate);
-					list.add(dpred);
-					labelMapping.put(dpred, evPredicate);
-				} else {
+				if (evPredicate.getSource() instanceof IInvariant) {  // test can fail for generated invariants
+                    final IInvariant ucp = (IInvariant) evPredicate.getSource(); // comments only attached in unchecked source
+                    if (ucp.hasAttribute(EventBAttributes.COMMENT_ATTRIBUTE)) {
+                        final String commentString = ucp.getAttributeValue(EventBAttributes.COMMENT_ATTRIBUTE);
+                        //System.out.println("Invariant/theorem " + predicate + " has description " + commentString);
+                        final TPragmaFreeText desc = new TPragmaFreeText(commentString);
+                        ADescriptionPragma descPragma = new ADescriptionPragma(Collections.singletonList(desc));
+                        ADescriptionPredicate dpred = new ADescriptionPredicate(descPragma, predicate);
+                        list.add(dpred);
+                        labelMapping.put(dpred, evPredicate);
+                    } else {
+                        list.add(predicate);
+                        labelMapping.put(predicate, evPredicate);
+                    }
+				} else { // cannot cast source to IInvariant
 					list.add(predicate);
 					labelMapping.put(predicate, evPredicate);
 				}
-- 
GitLab