Both types of engine now disallow negative/infinite/NaN rewards. Symbolic engines will mostly still not detect the presence of NaN due to the way that CUDD deals with this. Regression tests also added.