(1) removed abstraction shortcut that was not fully sound
(2) strengthened checker to perform less backwards propagations