This is a change requested by @NikolajBjorner ( 5f8c97532c (commitcomment-26049417) ).
5f8c97532c (commitcomment-26049417)