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.");
                             }
                         }
diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp
index 1a005d2d0..905fbffa9 100644
--- a/src/storm/storage/SparseMatrix.cpp
+++ b/src/storm/storage/SparseMatrix.cpp
@@ -1571,7 +1571,7 @@ namespace storm {
         typename SparseMatrix<ValueType>::index_type SparseMatrix<ValueType>::getNonconstantRowGroupCount() const {
             index_type nonConstRowGroups = 0;
             for (index_type rowGroup=0; rowGroup < this->getRowGroupCount(); ++rowGroup) {
-                for( auto const& entry : this->getRowGroup(rowGroup)){
+                for (auto const& entry : this->getRowGroup(rowGroup)){
                     if(!storm::utility::isConstant(entry.getValue())){
                         ++nonConstRowGroups;
                         break;
@@ -1584,11 +1584,18 @@ namespace storm {
         template<typename ValueType>
         bool SparseMatrix<ValueType>::isProbabilistic() const {
             storm::utility::ConstantsComparator<ValueType> comparator;
-            for(index_type row = 0; row < this->rowCount; ++row) {
+            for (index_type row = 0; row < this->rowCount; ++row) {
                 if(!comparator.isOne(getRowSum(row))) {
                     return false;
                 }
             }
+            for (auto const& entry : *this) {
+                if (comparator.isConstant(entry.getValue())) {
+                    if (comparator.isLess(entry.getValue(), storm::utility::zero<ValueType>())) {
+                        return false;
+                    }
+                }
+            }
             return true;
         }
         
diff --git a/src/storm/storage/prism/Update.cpp b/src/storm/storage/prism/Update.cpp
index 86693328c..0d1fce1ce 100644
--- a/src/storm/storage/prism/Update.cpp
+++ b/src/storm/storage/prism/Update.cpp
@@ -2,6 +2,7 @@
 
 #include <algorithm>
 #include <boost/algorithm/string/join.hpp>
+#include <storm/exceptions/IllegalArgumentException.h>
 
 #include "storm/utility/macros.h"
 #include "storm/exceptions/OutOfRangeException.h"
@@ -9,6 +10,7 @@
 namespace storm {
     namespace prism {
         Update::Update(uint_fast64_t globalIndex, storm::expressions::Expression const& likelihoodExpression, std::vector<storm::prism::Assignment> const& assignments, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), likelihoodExpression(likelihoodExpression), assignments(assignments), variableToAssignmentIndexMap(), globalIndex(globalIndex) {
+            STORM_LOG_ASSERT(likelihoodExpression.containsVariables() || likelihoodExpression.evaluateAsRational() >= 0, "Negative likelihood expressions are not allowed.");
             std::sort(this->assignments.begin(), this->assignments.end(), [] (storm::prism::Assignment const& assignment1, storm::prism::Assignment const& assignment2) {
                 bool smaller = assignment1.getVariable().getType().isBooleanType() && !assignment2.getVariable().getType().isBooleanType();
                 if (!smaller) {
@@ -64,9 +66,10 @@ namespace storm {
             for (auto const& assignment : this->getAssignments()) {
                 newAssignments.emplace_back(assignment.substitute(substitution));
             }
-            
+            auto newLikelihoodExpression = this->getLikelihoodExpression().substitute(substitution);
+            STORM_LOG_THROW(likelihoodExpression.containsVariables() || likelihoodExpression.evaluateAsRational() >= 0, storm::exceptions::IllegalArgumentException, "Substitution yielding negative probabilities in '" << this->getLikelihoodExpression() << "' are not allowed.");
             // FIXME: The expression could be simplified, but 1/K (where K is an int) is then resolved to 0, which is incorrect (for probabilities).
-            return Update(this->getGlobalIndex(), this->getLikelihoodExpression().substitute(substitution), newAssignments, this->getFilename(), this->getLineNumber());
+            return Update(this->getGlobalIndex(), newLikelihoodExpression, newAssignments, this->getFilename(), this->getLineNumber());
         }
         
         Update Update::removeIdentityAssignments() const {