Updates based on presentation feedback

Fixed a contradiction on WCET, refactored some of the constraints to
speed up the solvers and reduce the burden on large numbers.