diff --git a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java
index b832920fd..7f9978a66 100644
--- a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java
+++ b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java
@@ -36,20 +36,24 @@
 import java.util.Map;
 import java.util.Vector;
 
+import com.fujitsu.vdmj.Settings;
 import com.fujitsu.vdmj.ast.lex.LexBooleanToken;
 import com.fujitsu.vdmj.in.INNode;
+import com.fujitsu.vdmj.in.definitions.INClassDefinition;
 import com.fujitsu.vdmj.in.expressions.INBooleanLiteralExpression;
 import com.fujitsu.vdmj.in.expressions.INExpression;
 import com.fujitsu.vdmj.in.patterns.INBindingSetter;
+import com.fujitsu.vdmj.lex.Dialect;
 import com.fujitsu.vdmj.mapper.ClassMapper;
 import com.fujitsu.vdmj.po.annotations.POAnnotation;
 import com.fujitsu.vdmj.pog.POStatus;
 import com.fujitsu.vdmj.pog.ProofObligation;
 import com.fujitsu.vdmj.pog.ProofObligationList;
+import com.fujitsu.vdmj.runtime.ClassInterpreter;
 import com.fujitsu.vdmj.runtime.Context;
 import com.fujitsu.vdmj.runtime.ContextException;
 import com.fujitsu.vdmj.runtime.Interpreter;
-import com.fujitsu.vdmj.runtime.RootContext;
+import com.fujitsu.vdmj.runtime.ObjectContext;
 import com.fujitsu.vdmj.tc.expressions.TCExistsExpression;
 import com.fujitsu.vdmj.tc.expressions.TCExpression;
 import com.fujitsu.vdmj.tc.lex.TCNameToken;
@@ -58,6 +62,7 @@
 import com.fujitsu.vdmj.tc.types.TCType;
 import com.fujitsu.vdmj.util.GetResource;
 import com.fujitsu.vdmj.values.BooleanValue;
+import com.fujitsu.vdmj.values.ObjectValue;
 import com.fujitsu.vdmj.values.ParameterValue;
 import com.fujitsu.vdmj.values.Value;
 import com.fujitsu.vdmj.values.ValueList;
@@ -362,7 +367,6 @@ public void checkObligation(ProofObligation po, Results results)
 		try
 		{
 			resetErrors();	// Only flag fatal errors
-			RootContext ctxt = Interpreter.getInstance().getInitialContext();
 			INExpression poexp = getINExpression(po);
 			List<INBindingSetter> bindings = getINBindList(poexp);;
 
@@ -408,6 +412,20 @@ else if (results.proved &&
 				long before = System.currentTimeMillis();
 				Value result = new BooleanValue(false);
 				ContextException exception = null;
+				Context ctxt = Interpreter.getInstance().getInitialContext();
+				
+				if (Settings.dialect != Dialect.VDM_SL)
+				{
+					ClassInterpreter in = ClassInterpreter.getInstance();
+					INClassDefinition classdef = in.getDefaultClass();
+					ObjectValue object = classdef.newInstance(null, null, ctxt);
+
+					ctxt = new ObjectContext(
+							classdef.name.getLocation(), classdef.name.getName() + "()",
+							ctxt, object);
+
+					ctxt.put(classdef.name.getSelfName(), object);
+				}
 				
 				IterableContext ictxt = addTypeParams(po, ctxt);
 
diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ClassInterpreter.java b/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ClassInterpreter.java
index 81f8683fa..54237d156 100644
--- a/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ClassInterpreter.java
+++ b/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ClassInterpreter.java
@@ -160,6 +160,11 @@ public String getDefaultName()
 	{
 		return defaultClass.name.getName();
 	}
+	
+	public INClassDefinition getDefaultClass()
+	{
+		return defaultClass;
+	}
 
 	@Override
 	public File getDefaultFile()
diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ModuleInterpreter.java b/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ModuleInterpreter.java
index 207c97e61..e68a0b83a 100644
--- a/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ModuleInterpreter.java
+++ b/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ModuleInterpreter.java
@@ -174,6 +174,11 @@ public String getDefaultName()
 	{
 		return defaultModule.name.getName();
 	}
+	
+	public INModule getDefaultModule()
+	{
+		return defaultModule;
+	}
 
 	/**
 	 * @return The current default module's file name.