A bunch of new reasoning techniques in the Slant solver, leading to