From 6ba09b315d2c60b1fea43dd3a642a16b8c21c680 Mon Sep 17 00:00:00 2001
From: nick_battle <nick.battle@gmail.com>
Date: Thu, 24 Oct 2024 21:42:01 +0100
Subject: [PATCH] Fix PP PO names

---
 .../com/fujitsu/vdmj/po/definitions/POClassDefinition.java   | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POClassDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POClassDefinition.java
index 69762ff46..843d9b829 100644
--- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POClassDefinition.java
+++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POClassDefinition.java
@@ -29,6 +29,7 @@
 import com.fujitsu.vdmj.po.statements.POClassInvariantStatement;
 import com.fujitsu.vdmj.pog.POContextStack;
 import com.fujitsu.vdmj.pog.POGState;
+import com.fujitsu.vdmj.pog.PONameContext;
 import com.fujitsu.vdmj.pog.ProofObligationList;
 import com.fujitsu.vdmj.tc.definitions.TCClassDefinition;
 import com.fujitsu.vdmj.tc.lex.TCNameToken;
@@ -183,7 +184,9 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog
 
 		for (PODefinition def: definitions)
 		{
-			list.addAll(def.getProofObligations(new POContextStack(), new POGState(), local));
+			ctxt.push(new PONameContext(def.getVariableNames()));
+			list.addAll(def.getProofObligations(ctxt, new POGState(), local));
+			ctxt.pop();
 		}
 		
 		list.typeCheck(tcdef.name, local);