diff --git a/src/storm/analysis/GraphConditions.cpp b/src/storm/analysis/GraphConditions.cpp
index 812429dec..fb7b9e84a 100644
--- a/src/storm/analysis/GraphConditions.cpp
+++ b/src/storm/analysis/GraphConditions.cpp
@@ -29,14 +29,14 @@ namespace storm {
                 if (!storm::utility::isConstant(entry)) {
                     if (entry.denominator().isConstant()) {
                         if (entry.denominatorAsNumber() > 0) {
-                            wellformedConstraintSet.emplace(entry.nominator().polynomial(), storm::CompareRelation::GEQ);
+                            wellformedConstraintSet.emplace(entry.nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ);
                         } else if (entry.denominatorAsNumber() < 0) {
-                            wellformedConstraintSet.emplace(entry.nominator().polynomial(), storm::CompareRelation::LEQ);
+                            wellformedConstraintSet.emplace(entry.nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ);
                         } else {
                             assert(false); // Should fail before.
                         }
                     } else {
-                        wellformedConstraintSet.emplace(entry.denominator().polynomial(), storm::CompareRelation::NEQ);
+                        wellformedConstraintSet.emplace(entry.denominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ);
                         STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Rational functions at state rewards not yet supported.");
                     }
                 }
@@ -52,34 +52,35 @@ namespace storm {
                     if (!storm::utility::isConstant(transition.getValue())) {
                         // Assert: 0 <= transition <= 1
                         if (transition.getValue().denominator().isConstant()) {
+                            assert(transition.getValue().denominator().constantPart() != 0);
                             if (transition.getValue().denominator().constantPart() > 0) {
                                 // Assert: nom <= denom
-                                wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomial(), storm::CompareRelation::LEQ);
+                                wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomialWithCoefficient(), storm::CompareRelation::LEQ);
                                 // Assert: nom >= 0
-                                wellformedConstraintSet.emplace(transition.getValue().nominator().polynomial(), storm::CompareRelation::GEQ);
+                                wellformedConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ);
                             } else if (transition.getValue().denominator().constantPart() < 0) {
                                 // Assert nom >= denom
-                                wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomial(), storm::CompareRelation::GEQ);
+                                wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomialWithCoefficient(), storm::CompareRelation::GEQ);
                                 // Assert: nom <= 0
-                                wellformedConstraintSet.emplace(transition.getValue().nominator().polynomial(), storm::CompareRelation::LEQ);
+                                wellformedConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ);
                             } else {
                                 STORM_LOG_ASSERT(false, "Denominator must not equal 0.");
                             }
                         } else {
                             // Assert: denom != 0
-                            wellformedConstraintSet.emplace(transition.getValue().denominator().polynomial(), storm::CompareRelation::NEQ);
+                            wellformedConstraintSet.emplace(transition.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ);
                              // Assert: transition >= 0 <==> if denom > 0 then nom >= 0 else nom <= 0
-                            wellformedConstraintSet.emplace(carl::FormulaType::ITE, typename ConstraintType<ValueType>::val(transition.getValue().denominator().polynomial(), storm::CompareRelation::GREATER), typename ConstraintType<ValueType>::val(transition.getValue().nominator().polynomial(), storm::CompareRelation::GEQ), typename ConstraintType<ValueType>::val(transition.getValue().nominator().polynomial(), storm::CompareRelation::LEQ));
+                            wellformedConstraintSet.emplace(carl::FormulaType::ITE, typename ConstraintType<ValueType>::val(transition.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::GREATER), typename ConstraintType<ValueType>::val(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ), typename ConstraintType<ValueType>::val(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ));
                              // TODO: Assert: transition <= 1 <==> if denom > 0 then nom - denom <= 0 else nom - denom >= 0
                         }
                         // Assert: transition > 0
-                        graphPreservingConstraintSet.emplace(transition.getValue().nominator().polynomial(), storm::CompareRelation::NEQ);
+                        graphPreservingConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ);
                     }
                 }
                 STORM_LOG_ASSERT(!storm::utility::isConstant(sum) || storm::utility::isOne(sum), "If the sum is a constant, it must be equal to 1.");
                 if(!storm::utility::isConstant(sum)) {
                     // Assert: sum == 1
-                    wellformedConstraintSet.emplace((sum.nominator() - sum.denominator()).polynomial(), storm::CompareRelation::EQ);
+                    wellformedConstraintSet.emplace((sum.nominator() - sum.denominator()).polynomialWithCoefficient(), storm::CompareRelation::EQ);
                 }
 
             }
@@ -95,14 +96,14 @@ namespace storm {
                         if(!entry.getValue().isConstant()) {
                             if (entry.getValue().denominator().isConstant()) {
                                 if (entry.getValue().denominatorAsNumber() > 0) {
-                                    wellformedConstraintSet.emplace(entry.getValue().nominator().polynomial(), storm::CompareRelation::GEQ);
+                                    wellformedConstraintSet.emplace(entry.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ);
                                 } else if (entry.getValue().denominatorAsNumber() < 0) {
-                                    wellformedConstraintSet.emplace(entry.getValue().nominator().polynomial(), storm::CompareRelation::LEQ);
+                                    wellformedConstraintSet.emplace(entry.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ);
                                 } else {
                                     assert(false); // Should fail before.
                                 }
                             } else {
-                                wellformedConstraintSet.emplace(entry.getValue().denominator().polynomial(), storm::CompareRelation::NEQ);
+                                wellformedConstraintSet.emplace(entry.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ);
                                 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Rational functions at transition rewards are not yet supported.");
                             }
                         }