public int findNextLeafMaxVersion() {
		if (pos < 0) {
			throw new RuntimeException("findNext called after exploration is finished");
		}

		int node = indices[pos];
		if (ddmanager.isleaf(node)) {
			throw new RuntimeException("findNext went too far");
		}
		
		int curValue = values[pos];
		MDDVariable var = ddmanager.getNodeVariable(node);
		if (curValue >= 0) {
			int child = ddmanager.getChild(node, curValue);


			for ( curValue++ ; curValue<var.nbval ; curValue++) {
				int curChild = ddmanager.getChild(node, curValue);
				if (curChild != child) {
					break;
				}
			}
		} else {
			curValue++;
		}
		
		if (curValue < var.nbval) {
			values[pos] = curValue;
			int next = ddmanager.getChild(node, curValue);
			if (ddmanager.isleaf(next)) {
				return next;
			}
			pos++;
			indices[pos] = next;
			values[pos] = -1;
		} else {
			pos--;
			if (pos < 0) {
				return -1;
			}
		}
		return findNextLeafMaxVersion();
	}