Using the infrastructure from the previous commit, we request exact evaluation of constants in exact and parametric model checking mode. Additionally, note where we deliberately choose non-exact evaluation mode. Add corresponding test cases.