(1) some refactorings
(2) added a new type check in the backwards solver
(3) added some more test cases