Refined the constraint solver to not use substitutions. This finishes the transition of sizeof to an uninterpreted function.