diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c
index caf2ad18d..55c78e4f5 100644
--- a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c
+++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c
@@ -606,7 +606,7 @@ TASK_IMPL_2(MTBDD, mtbdd_op_sharpen, MTBDD, a, size_t, p)
             MTBDD result = mtbdd_storm_rational_number(storm_double_sharpen(mtbdd_getdouble(a), p));
             return result;
         } else if (mtbddnode_gettype(na) == srn_type) {
-            return mtbdd_storm_rational_number(storm_rational_number_sharpen((storm_rational_number_ptr)mtbdd_getstorm_rational_function_ptr(a), p));
+            return mtbdd_storm_rational_number(storm_rational_number_sharpen((storm_rational_number_ptr)mtbdd_getstorm_rational_number_ptr(a), p));
         } else {
             printf("ERROR: Unsupported value type in sharpen.\n");
             assert(0);
diff --git a/src/storm/solver/SymbolicEquationSolver.cpp b/src/storm/solver/SymbolicEquationSolver.cpp
index a76f94873..cf5efc71e 100644
--- a/src/storm/solver/SymbolicEquationSolver.cpp
+++ b/src/storm/solver/SymbolicEquationSolver.cpp
@@ -62,7 +62,47 @@ namespace storm {
         }
         
         template<storm::dd::DdType DdType, typename ValueType>
-        storm::dd::Add<DdType, ValueType> SymbolicEquationSolver<DdType, ValueType>::getLowerBounds() const {
+        bool SymbolicEquationSolver<DdType, ValueType>::hasLowerBound() const {
+            return static_cast<bool>(lowerBound);
+        }
+        
+        template<storm::dd::DdType DdType, typename ValueType>
+        ValueType const& SymbolicEquationSolver<DdType, ValueType>::getLowerBound() const {
+            return lowerBound.get();
+        }
+        
+        template<storm::dd::DdType DdType, typename ValueType>
+        bool SymbolicEquationSolver<DdType, ValueType>::hasLowerBounds() const {
+            return static_cast<bool>(lowerBounds);
+        }
+        
+        template<storm::dd::DdType DdType, typename ValueType>
+        storm::dd::Add<DdType, ValueType> const& SymbolicEquationSolver<DdType, ValueType>::getLowerBounds() const {
+            return lowerBounds.get();
+        }
+        
+        template<storm::dd::DdType DdType, typename ValueType>
+        bool SymbolicEquationSolver<DdType, ValueType>::hasUpperBound() const {
+            return static_cast<bool>(upperBound);
+        }
+        
+        template<storm::dd::DdType DdType, typename ValueType>
+        ValueType const& SymbolicEquationSolver<DdType, ValueType>::getUpperBound() const {
+            return upperBound.get();
+        }
+        
+        template<storm::dd::DdType DdType, typename ValueType>
+        bool SymbolicEquationSolver<DdType, ValueType>::hasUpperBounds() const {
+            return static_cast<bool>(upperBounds);
+        }
+        
+        template<storm::dd::DdType DdType, typename ValueType>
+        storm::dd::Add<DdType, ValueType> const& SymbolicEquationSolver<DdType, ValueType>::getUpperBounds() const {
+            return upperBounds.get();
+        }
+        
+        template<storm::dd::DdType DdType, typename ValueType>
+        storm::dd::Add<DdType, ValueType> SymbolicEquationSolver<DdType, ValueType>::getLowerBoundsVector() const {
             STORM_LOG_THROW(lowerBound || lowerBounds, storm::exceptions::UnmetRequirementException, "Requiring lower bounds, but did not get any.");
             if (lowerBounds) {
                 return lowerBounds.get();
@@ -72,7 +112,7 @@ namespace storm {
         }
         
         template<storm::dd::DdType DdType, typename ValueType>
-        storm::dd::Add<DdType, ValueType> SymbolicEquationSolver<DdType, ValueType>::getUpperBounds() const {
+        storm::dd::Add<DdType, ValueType> SymbolicEquationSolver<DdType, ValueType>::getUpperBoundsVector() const {
             STORM_LOG_THROW(upperBound || upperBounds, storm::exceptions::UnmetRequirementException, "Requiring upper bounds, but did not get any.");
             if (upperBounds) {
                 return upperBounds.get();
diff --git a/src/storm/solver/SymbolicEquationSolver.h b/src/storm/solver/SymbolicEquationSolver.h
index 2e6322cfc..73681d762 100644
--- a/src/storm/solver/SymbolicEquationSolver.h
+++ b/src/storm/solver/SymbolicEquationSolver.h
@@ -14,22 +14,31 @@ namespace storm {
             SymbolicEquationSolver() = default;
             SymbolicEquationSolver(storm::dd::Bdd<DdType> const& allRows);
 
-            void setLowerBounds(storm::dd::Add<DdType, ValueType> const& lowerBounds);
-            void setLowerBound(ValueType const& lowerBound);
-            void setUpperBounds(storm::dd::Add<DdType, ValueType> const& upperBounds);
-            void setUpperBound(ValueType const& lowerBound);
-            void setBounds(ValueType const& lowerBound, ValueType const& upperBound);
-            void setBounds(storm::dd::Add<DdType, ValueType> const& lowerBounds, storm::dd::Add<DdType, ValueType> const& upperBounds);
-            
+            virtual void setLowerBounds(storm::dd::Add<DdType, ValueType> const& lowerBounds);
+            virtual void setLowerBound(ValueType const& lowerBound);
+            virtual void setUpperBounds(storm::dd::Add<DdType, ValueType> const& upperBounds);
+            virtual void setUpperBound(ValueType const& lowerBound);
+            virtual void setBounds(ValueType const& lowerBound, ValueType const& upperBound);
+            virtual void setBounds(storm::dd::Add<DdType, ValueType> const& lowerBounds, storm::dd::Add<DdType, ValueType> const& upperBounds);
+
+            bool hasLowerBound() const;
+            ValueType const& getLowerBound() const;
+            bool hasLowerBounds() const;
+            storm::dd::Add<DdType, ValueType> const& getLowerBounds() const;
+            bool hasUpperBound() const;
+            ValueType const& getUpperBound() const;
+            bool hasUpperBounds() const;
+            storm::dd::Add<DdType, ValueType> const& getUpperBounds() const;
+
             /*!
              * Retrieves a vector of lower bounds for all values (if any lower bounds are known).
              */
-            storm::dd::Add<DdType, ValueType> getLowerBounds() const;
+            storm::dd::Add<DdType, ValueType> getLowerBoundsVector() const;
             
             /*!
              * Retrieves a vector of upper bounds for all values (if any lower bounds are known).
              */
-            storm::dd::Add<DdType, ValueType> getUpperBounds() const;
+            storm::dd::Add<DdType, ValueType> getUpperBoundsVector() const;
 
         protected:
             storm::dd::DdManager<DdType>& getDdManager() const;
diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp
index 4cb05ee90..2df70a371 100644
--- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp
+++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp
@@ -226,7 +226,7 @@ namespace storm {
         template<storm::dd::DdType DdType, typename ValueType>
         template<typename ImpreciseType>
         typename std::enable_if<std::is_same<ValueType, ImpreciseType>::value && storm::NumberTraits<ValueType>::IsExact, storm::dd::Add<DdType, ValueType>>::type SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::solveEquationsRationalSearchHelper(storm::solver::OptimizationDirection const& dir, storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const {
-            return solveEquationsRationalSearchHelper<ValueType, ValueType>(dir, *this, *this, b, this->getLowerBounds(), b);
+            return solveEquationsRationalSearchHelper<ValueType, ValueType>(dir, *this, *this, b, this->getLowerBoundsVector(), b);
         }
         
         template<storm::dd::DdType DdType, typename ValueType>
@@ -236,7 +236,7 @@ namespace storm {
             storm::dd::Add<DdType, storm::RationalNumber> rationalB = b.template toValueType<storm::RationalNumber>();
             SymbolicMinMaxLinearEquationSolver<DdType, storm::RationalNumber> rationalSolver(this->A.template toValueType<storm::RationalNumber>(), this->allRows, this->illegalMask, this->rowMetaVariables, this->columnMetaVariables, this->choiceVariables, this->rowColumnMetaVariablePairs, std::make_unique<GeneralSymbolicLinearEquationSolverFactory<DdType, storm::RationalNumber>>());
             
-            storm::dd::Add<DdType, storm::RationalNumber> rationalResult = solveEquationsRationalSearchHelper<storm::RationalNumber, ImpreciseType>(dir, rationalSolver, *this, rationalB, this->getLowerBounds(), b);
+            storm::dd::Add<DdType, storm::RationalNumber> rationalResult = solveEquationsRationalSearchHelper<storm::RationalNumber, ImpreciseType>(dir, rationalSolver, *this, rationalB, this->getLowerBoundsVector(), b);
             return rationalResult.template toValueType<ValueType>();
         }
 
@@ -248,7 +248,7 @@ namespace storm {
             storm::dd::Add<DdType, ValueType> rationalResult;
             storm::dd::Add<DdType, ImpreciseType> impreciseX;
             try {
-                impreciseX = this->getLowerBounds().template toValueType<ImpreciseType>();
+                impreciseX = this->getLowerBoundsVector().template toValueType<ImpreciseType>();
                 storm::dd::Add<DdType, ImpreciseType> impreciseB = b.template toValueType<ImpreciseType>();
                 SymbolicMinMaxLinearEquationSolver<DdType, ImpreciseType> impreciseSolver(this->A.template toValueType<ImpreciseType>(), this->allRows, this->illegalMask, this->rowMetaVariables, this->columnMetaVariables, this->choiceVariables, this->rowColumnMetaVariablePairs, std::make_unique<GeneralSymbolicLinearEquationSolverFactory<DdType, ImpreciseType>>());
                 
@@ -276,7 +276,7 @@ namespace storm {
             if (this->hasInitialScheduler()) {
                 localX = solveEquationsWithScheduler(this->getInitialScheduler(), x, b);
             } else {
-                localX = this->getLowerBounds();
+                localX = this->getLowerBoundsVector();
             }
             
             ValueIterationResult viResult = performValueIteration(dir, localX, b, this->getSettings().getPrecision(), this->getSettings().getRelativeTerminationCriterion(), this->settings.getMaximalNumberOfIterations());
@@ -294,6 +294,7 @@ namespace storm {
         storm::dd::Add<DdType, ValueType>  SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::solveEquationsWithScheduler(storm::dd::Bdd<DdType> const& scheduler, storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const {
             
             std::unique_ptr<SymbolicLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory->create(this->allRows, this->rowMetaVariables, this->columnMetaVariables, this->rowColumnMetaVariablePairs);
+            this->forwardBounds(*solver);
             storm::dd::Add<DdType, ValueType> diagonal = (storm::utility::dd::getRowColumnDiagonal<DdType>(x.getDdManager(), this->rowColumnMetaVariablePairs) && this->allRows).template toAdd<ValueType>();
             return solveEquationsWithScheduler(*solver, scheduler, x, b, diagonal);
         }
@@ -327,6 +328,7 @@ namespace storm {
             
             // Initialize linear equation solver.
             std::unique_ptr<SymbolicLinearEquationSolver<DdType, ValueType>> linearEquationSolver = linearEquationSolverFactory->create(this->allRows, this->rowMetaVariables, this->columnMetaVariables, this->rowColumnMetaVariablePairs);
+            this->forwardBounds(*linearEquationSolver);
             
             // Iteratively solve and improve the scheduler.
             while (!converged && iterations < this->settings.getMaximalNumberOfIterations()) {
@@ -452,6 +454,22 @@ namespace storm {
         SymbolicMinMaxLinearEquationSolverSettings<ValueType> const& SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::getSettings() const {
             return settings;
         }
+        
+        template<storm::dd::DdType DdType, typename ValueType>
+        void SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::forwardBounds(storm::solver::SymbolicLinearEquationSolver<DdType, ValueType>& solver) const {
+            if (this->hasLowerBound()) {
+                solver.setLowerBound(this->getLowerBound());
+            }
+            if (this->hasLowerBounds()) {
+                solver.setLowerBounds(this->getLowerBounds());
+            }
+            if (this->hasUpperBound()) {
+                solver.setUpperBound(this->getUpperBound());
+            }
+            if (this->hasUpperBounds()) {
+                solver.setUpperBounds(this->getUpperBounds());
+            }
+        }
 
         template<storm::dd::DdType DdType, typename ValueType>
         MinMaxLinearEquationSolverRequirements SymbolicMinMaxLinearEquationSolverFactory<DdType, ValueType>::getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction) const {
diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h
index 4e5fadbfd..6853582f1 100644
--- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h
+++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h
@@ -213,6 +213,12 @@ namespace storm {
             
             // A scheduler that specifies with which schedulers to start.
             boost::optional<storm::dd::Bdd<DdType>> initialScheduler;
+            
+        private:
+            /*!
+             * Forwards the known bounds of this solver to the given linear equation solver.
+             */
+            void forwardBounds(storm::solver::SymbolicLinearEquationSolver<DdType, ValueType>& solver) const;
         };
         
         template<storm::dd::DdType DdType, typename ValueType>
diff --git a/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp b/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp
index 5f3613100..5c6da4572 100644
--- a/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp
+++ b/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp
@@ -185,7 +185,7 @@ namespace storm {
         
         template<storm::dd::DdType DdType, typename ValueType>
         storm::dd::Add<DdType, ValueType> SymbolicNativeLinearEquationSolver<DdType, ValueType>::solveEquationsPower(storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const {
-            PowerIterationResult result = performPowerIteration(this->getLowerBounds(), b, this->getSettings().getPrecision(), this->getSettings().getRelativeTerminationCriterion(), this->getSettings().getMaximalNumberOfIterations());
+            PowerIterationResult result = performPowerIteration(this->getLowerBoundsVector(), b, this->getSettings().getPrecision(), this->getSettings().getRelativeTerminationCriterion(), this->getSettings().getMaximalNumberOfIterations());
             
             if (result.status == SolverStatus::Converged) {
                 STORM_LOG_INFO("Iterative solver (power iteration) converged in " << result.iterations << " iterations.");
@@ -195,7 +195,7 @@ namespace storm {
             
             return result.values;
         }
-        
+
         template<storm::dd::DdType DdType, typename ValueType>
         bool SymbolicNativeLinearEquationSolver<DdType, ValueType>::isSolutionFixedPoint(storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const {
             storm::dd::Add<DdType, ValueType> xAsColumn = x.swapVariables(this->rowColumnMetaVariablePairs);
@@ -273,7 +273,7 @@ namespace storm {
         template<storm::dd::DdType DdType, typename ValueType>
         template<typename ImpreciseType>
         typename std::enable_if<std::is_same<ValueType, ImpreciseType>::value && storm::NumberTraits<ValueType>::IsExact, storm::dd::Add<DdType, ValueType>>::type SymbolicNativeLinearEquationSolver<DdType, ValueType>::solveEquationsRationalSearchHelper(storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const {
-            return solveEquationsRationalSearchHelper<ValueType, ValueType>(*this, *this, b, this->getLowerBounds(), b);
+            return solveEquationsRationalSearchHelper<ValueType, ValueType>(*this, *this, b, this->getLowerBoundsVector(), b);
         }
         
         template<storm::dd::DdType DdType, typename ValueType>
@@ -283,7 +283,7 @@ namespace storm {
             storm::dd::Add<DdType, storm::RationalNumber> rationalB = b.template toValueType<storm::RationalNumber>();
             SymbolicNativeLinearEquationSolver<DdType, storm::RationalNumber> rationalSolver(this->A.template toValueType<storm::RationalNumber>(), this->allRows, this->rowMetaVariables, this->columnMetaVariables, this->rowColumnMetaVariablePairs);
             
-            storm::dd::Add<DdType, storm::RationalNumber> rationalResult = solveEquationsRationalSearchHelper<storm::RationalNumber, ImpreciseType>(rationalSolver, *this, rationalB, this->getLowerBounds(), b);
+            storm::dd::Add<DdType, storm::RationalNumber> rationalResult = solveEquationsRationalSearchHelper<storm::RationalNumber, ImpreciseType>(rationalSolver, *this, rationalB, this->getLowerBoundsVector(), b);
             return rationalResult.template toValueType<ValueType>();
         }
         
@@ -295,7 +295,7 @@ namespace storm {
             storm::dd::Add<DdType, ValueType> rationalResult;
             storm::dd::Add<DdType, ImpreciseType> impreciseX;
             try {
-                impreciseX = this->getLowerBounds().template toValueType<ImpreciseType>();
+                impreciseX = this->getLowerBoundsVector().template toValueType<ImpreciseType>();
                 storm::dd::Add<DdType, ImpreciseType> impreciseB = b.template toValueType<ImpreciseType>();
                 SymbolicNativeLinearEquationSolver<DdType, ImpreciseType> impreciseSolver(this->A.template toValueType<ImpreciseType>(), this->allRows, this->rowMetaVariables, this->columnMetaVariables, this->rowColumnMetaVariablePairs);
                 
diff --git a/src/test/storm/storage/SylvanDdTest.cpp b/src/test/storm/storage/SylvanDdTest.cpp
index 48778a174..ddb937590 100644
--- a/src/test/storm/storage/SylvanDdTest.cpp
+++ b/src/test/storm/storage/SylvanDdTest.cpp
@@ -855,6 +855,26 @@ TEST(SylvanDd, AddSharpenTest) {
     ASSERT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("19/10")), sharpened.getValue(metaVariableToValueMap));
 }
 
+TEST(SylvanDd, AddRationalSharpenTest) {
+    std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::Sylvan>> manager(new storm::dd::DdManager<storm::dd::DdType::Sylvan>());
+    std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
+    
+    storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalNumber> dd = manager->template getAddOne<storm::RationalNumber>();
+    ASSERT_NO_THROW(dd.setValue(x.first, 4, storm::utility::convertNumber<storm::RationalNumber>(1.89999999)));
+    ASSERT_EQ(2ul, dd.getLeafCount());
+    
+    storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalNumber> sharpened = dd.sharpenKwekMehlhorn(1);
+    
+    std::map<storm::expressions::Variable, int_fast64_t> metaVariableToValueMap;
+    metaVariableToValueMap.emplace(x.first, 4);
+    
+    sharpened = dd.sharpenKwekMehlhorn(1);
+    ASSERT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("9/5")), sharpened.getValue(metaVariableToValueMap));
+    
+    sharpened = dd.sharpenKwekMehlhorn(2);
+    ASSERT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("19/10")), sharpened.getValue(metaVariableToValueMap));
+}
+
 TEST(SylvanDd, AddToRationalTest) {
     std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::Sylvan>> manager(new storm::dd::DdManager<storm::dd::DdType::Sylvan>());
     std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);