Fix getDefProofObligations to add context after each def's POs

nickbattle · Oct 24, 2024 · 0e22886 · 0e22886
1 parent 7fc1261
commit 0e22886
Showing 1 changed file with 2 additions and 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
@@ -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++)