predicate lex_minimize(array[int] of var int: o) =
	let {
		var min(index_set(o))..max(index_set(o))+1: stage;
	} in if status() = START then
		stage = min(index_set(o))
	elseif status() = UNSAT then
		stage = lastval(stage) + 1
	else /* status() = SAT */
		stage = lastval(stage)
		/\ o[stage] < sol(o[stage])
	endif
	/\ _objective = o[stage];
	/\ forall(i in min(index_set(o))..stage-1) (
		o[i] = sol(o[i])
	)
	/\ if stage > max(index_set(o)) then
		complete()
	endif;