This is similar in spirit to what was done in commit 8e590a117f. Signed-off-by: Rogério Brito <rbrito@ime.usp.br>
8e590a117f