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