From 0e22886bfeb9ac7a6da1f546f550006e28c4b623 Mon Sep 17 00:00:00 2001
From: Nick Battle <nick.battle@gmail.com>
Date: Thu, 24 Oct 2024 14:02:43 +0100
Subject: [PATCH] Fix getDefProofObligations to add context after each def's
 POs

---
 .../com/fujitsu/vdmj/po/definitions/PODefinitionList.java    | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinitionList.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinitionList.java
index 041d32956..9b1124f65 100644
--- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinitionList.java
+++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinitionList.java
@@ -99,10 +99,9 @@ public ProofObligationList getDefProofObligations(POContextStack ctxt, POGState
 
 		for (PODefinition d: this)
 		{
-			ctxt.push(new POLetDefContext(d));		// In scope for recursive or total obligations
-			count++;
-
 			obligations.addAll(d.getProofObligations(ctxt, pogState, env));
+			ctxt.push(new POLetDefContext(d));
+			count++;
 		}
 		
 		for (int i=0; i<count; i++)