diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
index 9844a64af..6df0210e9 100644
--- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
+++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
@@ -1531,12 +1531,17 @@ namespace storm {
                         }
                     }
                 }
-                    
+
+                std::set<std::string> expressionLabelStrings;
                 for (auto const& expression : this->options.getExpressionLabels()) {
                     cpptempl::data_map label;
-                    label["name"] = expression.toString();
-                    label["predicate"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(expression), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastDouble));
-                    labels.push_back(label);
+                    std::string expressionLabelString = expression.toString();
+                    if(expressionLabelStrings.count(expressionLabelString) == 0) {
+                        label["name"] = expression.toString();
+                        label["predicate"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(expression), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastDouble));
+                        labels.push_back(label);
+                        expressionLabelStrings.insert(expressionLabelString);
+                    }
                 }
                     
                 modelData["labels"] = cpptempl::make_data(labels);
diff --git a/src/storm/builder/jit/ModelComponentsBuilder.cpp b/src/storm/builder/jit/ModelComponentsBuilder.cpp
index 6c51840ad..6f61feb19 100644
--- a/src/storm/builder/jit/ModelComponentsBuilder.cpp
+++ b/src/storm/builder/jit/ModelComponentsBuilder.cpp
@@ -129,7 +129,7 @@ namespace storm {
                     return new storm::models::sparse::Dtmc<ValueType, storm::models::sparse::StandardRewardModel<ValueType>>(std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels));
                 } else if (modelType == storm::jani::ModelType::CTMC) {
                     return new storm::models::sparse::Ctmc<ValueType, storm::models::sparse::StandardRewardModel<ValueType>>(std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels));
-                } else if (modelType == storm::jani::ModelType::MDP) {
+                } else if (modelType == storm::jani::ModelType::MDP || modelType == storm::jani::ModelType::LTS) {
                     return new storm::models::sparse::Mdp<ValueType, storm::models::sparse::StandardRewardModel<ValueType>>(std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels));
                 } else if (modelType == storm::jani::ModelType::MA) {
                     std::vector<ValueType> exitRates(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h
index 1ac363c4d..827f1701e 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h
+++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h
@@ -31,6 +31,8 @@ namespace storm {
                                                           storm::storage::BitVector const& ecActions,
                                                           storm::storage::BitVector const& possiblyRecurrentStates);
                 
+                virtual ~SparseMaPcaaWeightVectorChecker() = default;
+
             private:
                 
                 /*
diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h
index aa0425c4f..8b56386c9 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h
+++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h
@@ -25,7 +25,9 @@ namespace storm {
                                                  storm::storage::BitVector const& actionsWithNegativeReward,
                                                  storm::storage::BitVector const& ecActions,
                                                  storm::storage::BitVector const& possiblyRecurrentStates);
-                
+
+                virtual ~SparseMdpPcaaWeightVectorChecker() = default;
+
             private:
                 
                 /*!
diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h
index d4f3ea32b..c250f257b 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h
+++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h
@@ -25,7 +25,8 @@ namespace storm {
                  */
                 SparsePcaaAchievabilityQuery(SparsePcaaPreprocessorReturnType<SparseModelType>& preprocessorResult);
                 
-                
+                virtual ~SparsePcaaAchievabilityQuery() = default;
+
                 /*
                  * Invokes the computation and retrieves the result
                  */
diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h
index 08256f3c7..b6361faff 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h
+++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h
@@ -25,6 +25,8 @@ namespace storm {
                  */
                 SparsePcaaParetoQuery(SparsePcaaPreprocessorReturnType<SparseModelType>& preprocessorResult);
                 
+                virtual ~SparsePcaaParetoQuery() = default;
+
                 
                 /*
                  * Invokes the computation and retrieves the result
diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h
index 3e72763f1..ca2d8c81a 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h
+++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h
@@ -25,7 +25,8 @@ namespace storm {
                  */
                 SparsePcaaQuantitativeQuery(SparsePcaaPreprocessorReturnType<SparseModelType>& preprocessorResult);
                 
-                
+                virtual ~SparsePcaaQuantitativeQuery() = default;
+
                 /*
                  * Invokes the computation and retrieves the result
                  */
diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h
index c0a891a13..e6404c9ac 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h
+++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h
@@ -22,6 +22,8 @@ namespace storm {
                 typedef std::vector<GeometryValueType> Point;
                 typedef std::vector<GeometryValueType> WeightVector;
                 
+                virtual ~SparsePcaaQuery() = default;
+                
                 /*
                  * Invokes the computation and retrieves the result
                  */
diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h
index 452f30189..d80eb4931 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h
+++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h
@@ -40,6 +40,8 @@ namespace storm {
                                                         storm::storage::BitVector const& ecActions,
                                                         storm::storage::BitVector const& possiblyRecurrentStates);
                 
+                virtual ~SparsePcaaWeightVectorChecker() = default;
+                
                 /*!
                  * - computes the maximal expected reward w.r.t. the weighted sum of the rewards of the individual objectives
                  * - extracts the scheduler that induces this maximum
diff --git a/src/storm/parser/JaniParser.cpp b/src/storm/parser/JaniParser.cpp
index 08df6b605..ecb3ed0ff 100644
--- a/src/storm/parser/JaniParser.cpp
+++ b/src/storm/parser/JaniParser.cpp
@@ -370,7 +370,7 @@ namespace storm {
                         STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Reward bounded properties are not supported by storm");
                     }
                     if (args[0]->isTrueFormula()) {
-                        return std::make_shared<storm::logic::EventuallyFormula const>(args[1], storm::logic::FormulaContext::Reward);
+                        return std::make_shared<storm::logic::EventuallyFormula const>(args[1], formulaContext);
                     } else {
                         return std::make_shared<storm::logic::UntilFormula const>(args[0], args[1]);
                     }