// Checks the postcondition when it is executed
private Result executeTest(Path.ID id, QCInterpreter interpreter, Decl.FunctionOrMethod dec, TestType testType, int numTest, BigInteger lowerLimit, BigInteger upperLimit) {
		// Get the method for generating test values
		GenerateTest testGen;
		try {
			if(testType == TestType.EXHAUSTIVE) {
				testGen = new ExhaustiveGenerateTest(dec.getParameters(), interpreter, numTest, lowerLimit, upperLimit);
			}
			else {
	            testGen = new RandomGenerateTest(dec.getParameters(), interpreter, numTest, lowerLimit, upperLimit);
			}
		} catch (IntegerRangeException e) {
			System.out.println("Integer range was invalid for the limits given.");
			return Result.ERRORS;
		}
		// Get the function's relevant header information
		NameID name = new NameID(id, dec.getName().get());
		Type.Callable type = dec.getType();
		Tuple<Expr> preconditions = dec.getRequires();
		Tuple<Expr> postconditions = dec.getEnsures();
		Tuple<Decl.Variable> inputParameters = dec.getParameters();
		Tuple<Decl.Variable> outputParameters = dec.getReturns();
		System.out.println("Name of the function/method: " + name.name());
//		System.out.println("FUNCTION PARAM TYPES "+ inputParameters);
//		System.out.println("PRECONDITION "+ preconditions);
//		System.out.println("POSTCONDITION "+ postconditions);
//		// Have to remove the pre and post conditions out of the 
//		// function so the function is executed without validation
//		// Validation will be conducted manually inside the function.
//		Tuple<Expr> empty = new Tuple<Expr>();		
//		dec.setOperand(4, empty); // Remove precondition
//		dec.setOperand(5, empty); // Remove postcondition
		boolean completedAll = false;
		int numSkipped = 0;
		int numPassed = 0;
		int numFailed = 0;
		for(int i=0; i < numTest; i++) {
			recursiveType.clear();
			// Stop execution if all possible combinations have been generated 
			// Can do this for methods as well as a new call stack is created each time
			if(testGen.exceedSize() && i != 0) {
				completedAll = true;
				break;
			}
			RValue[] paramValues = null;
			CallStack frame = interpreter.new CallStack();
			// Check the precondition
			try {
				paramValues = testGen.generateParameters();
				for(int j=0; j < inputParameters.size(); j++) {
					Decl.Variable parameter = inputParameters.get(j);
					frame.putLocal(parameter.getName(), paramValues[j]);
				}
				interpreter.checkInvariants(frame, preconditions);
			}
			catch(CannotGenerateException e) {
				System.out.println(e);
				return Result.ERRORS;
			}
			catch(AssertionError e){
				System.out.println("Pre-condition failed on input: " + Arrays.toString(paramValues));
				numSkipped++;
				continue;
			}
			catch(RuntimeException e) {
				System.out.println("Error occurred when generating input " + e + ": " + e.getMessage());
				return Result.ERRORS;
			}
			System.out.println("INPUT: " + Arrays.toString(paramValues));
			// Checks the postcondition when it is executed
			RValue[] returns = null;
			try {
				returns = interpreter.execute(name, type, frame, false, false, paramValues);
				recursiveType.clear();
			}
			catch(AssertionError e) {
				System.out.println("Error occurred during execution " + e + ": " + e.getMessage());
				numFailed++;
				continue;
			} 
			catch(RuntimeException e) {
				System.out.println("Error occurred during execution " + e + ": " + e.getMessage());
				return Result.ERRORS;
			}
			try {
				// Add the return values into the frame for validation
				for(int j=0; j < outputParameters.size(); j++) {
					Decl.Variable parameter = outputParameters.get(j);
					Type paramType = parameter.getType();
					boolean valid = checkInvariant(interpreter, paramType, returns[j]);
					if(!valid) {
						throw new AssertionError("Type constraints for " + parameter  + " failed");
					}
					frame.putLocal(parameter.getName(), returns[j]);
				}	
				try {
					interpreter.checkInvariants(frame, postconditions);
					numPassed++;
//					// Print out any return values produced
					if (returns != null) {
						System.out.println("OUTPUT: " + Arrays.toString(returns));
					}
				}
				catch(AssertionError e) {
					System.out.printf("Failed Input: %s%nFailed Output: %s%n", Arrays.toString(paramValues), Arrays.toString(returns));
					System.out.println("Postcondition failed " + e);
					numFailed++;
				} 
				catch(RuntimeException e) {
					System.out.println("Error when checking invariants of return values " + e + ": " + e.getMessage());
					return Result.ERRORS;
				}
			}
			catch(AssertionError e) {
				System.out.printf("Failed Input: %s%nFailed Output: %s%n", Arrays.toString(paramValues), Arrays.toString(returns));
				System.out.println("Due to error " + e);
				numFailed++;
			} 
			catch(RuntimeException e) {
				System.out.println("Error when checking type invariants of return values " + e + ": " + e.getMessage());
				return Result.ERRORS;
			}
			catch (ResolutionError e) {
				// FIXME resolution error
				e.printStackTrace();
				assert false;
			} 
		}
		// Overall test statistics
		if(completedAll) {
			System.out.println("Tested all possible combinations");
			int numActualTest = numPassed + numFailed + numSkipped;
			if(numFailed == 0) {
				if(numPassed > 0) {
					System.out.printf("Ok: %d passed  (%.2f %%), %d skipped (%.2f %%), ran %d tests %n",
							numPassed, (double) 100 * numPassed/numActualTest, numSkipped, (double) 100 * numSkipped/numActualTest, numActualTest);
					return Result.PASSED;
				}
				else {
					System.out.println("All tests skipped!");
					return Result.SKIPPED;
				}
			}
			System.out.printf("Failed: %d passed (%.2f %%), %d failed (%.2f %%), %d skipped (%.2f %%), ran %d tests%n",
					numPassed, (double) 100 * numPassed/numActualTest, numFailed, (double) 100 * numFailed/numActualTest, numSkipped, (double) 100 * numSkipped/numActualTest, numActualTest);
			return Result.FAILED;
		}
		else if(numPassed + numSkipped == numTest) {
			assert numFailed == 0;
			System.out.printf("Ok: %d passed  (%.2f %%), %d skipped (%.2f %%), ran %d tests %n",
					numPassed, (double) 100 * numPassed/numTest, numSkipped, (double) 100 * numSkipped/numTest, numTest);
			return Result.PASSED;
		}
		else if(numSkipped == numTest) {
			System.out.println("All tests skipped!");
			return Result.SKIPPED;
		}
		else {
			System.out.printf("Failed: %d passed (%.2f %%), %d failed (%.2f %%), %d skipped (%.2f %%), ran %d tests%n",
					numPassed, (double) 100 * numPassed/numTest, numFailed, (double) 100 * numFailed/numTest, numSkipped, (double) 100 * numSkipped/numTest, numTest);
			return Result.FAILED;
		}
	}
}
System.out.println("INPUT: " + Arrays.toString(paramValues));
// Checks the postcondition when it is executed
RValue[] returns = null;
try {
catch(AssertionError e){
System.out.println("Pre-condition failed on input: " + Arrays.toString(paramValues));
numSkipped++;
continue;
}
catch(RuntimeException e) {
System.out.println("Error occurred when generating input " + e + ": " + e.getMessage());
return Result.ERRORS;
}
System.out.println("INPUT: " + Arrays.toString(paramValues));
// Checks the postcondition when it is executed
RValue[] returns = null;
try {
returns = interpreter.execute(name, type, frame, false, false, paramValues);
recursiveType.clear();
}
catch(AssertionError e) {
System.out.println("Error occurred during execution " + e + ": " + e.getMessage());
numFailed++;
continue;
}
for(int j=0; j < inputParameters.size(); j++) {
Decl.Variable parameter = inputParameters.get(j);
frame.putLocal(parameter.getName(), paramValues[j]);
}
interpreter.checkInvariants(frame, preconditions);
}
catch(CannotGenerateException e) {
System.out.println(e);
return Result.ERRORS;
}
catch(AssertionError e){
System.out.println("Pre-condition failed on input: " + Arrays.toString(paramValues));
numSkipped++;
continue;
}
catch(RuntimeException e) {
System.out.println("Error occurred when generating input " + e + ": " + e.getMessage());
return Result.ERRORS;
}
System.out.println("INPUT: " + Arrays.toString(paramValues));
// Checks the postcondition when it is executed
RValue[] returns = null;
try {
returns = interpreter.execute(name, type, frame, false, false, paramValues);
recursiveType.clear();
}
catch(AssertionError e) {
System.out.println("Error occurred during execution " + e + ": " + e.getMessage());
numFailed++;
continue;
}
catch(RuntimeException e) {
System.out.println("Error occurred during execution " + e + ": " + e.getMessage());
return Result.ERRORS;
}
try {
// Add the return values into the frame for validation
for(int j=0; j < outputParameters.size(); j++) {
Decl.Variable parameter = outputParameters.get(j);
Type paramType = parameter.getType();
boolean valid = checkInvariant(interpreter, paramType, returns[j]);