diff --git a/src/storm-pars/analysis/AssumptionChecker.cpp b/src/storm-pars/analysis/AssumptionChecker.cpp
index 6727793c0..bba77fb37 100644
--- a/src/storm-pars/analysis/AssumptionChecker.cpp
+++ b/src/storm-pars/analysis/AssumptionChecker.cpp
@@ -2,15 +2,16 @@
 // Created by Jip Spel on 12.09.18.
 //
 
-#include <storm-pars/utility/ModelInstantiator.h>
-#include <storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h>
-#include <storm/exceptions/NotSupportedException.h>
+#include "storm-pars/utility/ModelInstantiator.h"
+#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
+#include "storm/exceptions/NotSupportedException.h"
 #include "AssumptionChecker.h"
 #include "storm/modelchecker/CheckTask.h"
 #include "storm/environment/Environment.h"
 #include "storm/modelchecker/results/CheckResult.h"
 #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
-
+#include "storm/storage/expressions/SimpleValuation.h"
+#include "storm/storage/expressions/ExpressionManager.h"
 
 
 
@@ -23,8 +24,6 @@ namespace storm {
             auto instantiator = storm::utility::ModelInstantiator<storm::models::sparse::Dtmc<ValueType>, storm::models::sparse::Dtmc<double>>(*model.get());
             auto matrix = model->getTransitionMatrix();
             std::set<storm::RationalFunctionVariable> variables =  storm::models::sparse::getProbabilityParameters(*model);
-
-
             for (auto i = 0; i < numberOfSamples; ++i) {
                 auto valuation = storm::utility::parametric::Valuation<ValueType>();
                 for (auto itr = variables.begin(); itr != variables.end(); ++itr) {
@@ -52,8 +51,8 @@ namespace storm {
                 std::vector<double> values = quantitativeResult.getValueVector();
                 results.push_back(values);
             }
-            this->numberOfStates = model->getNumberOfStates();
-            this->initialStates = model->getInitialStates();
+//            this->numberOfStates = model->getNumberOfStates();
+//            this->initialStates = model->getInitialStates();
         }
 
         template <typename ValueType>
@@ -67,6 +66,25 @@ namespace storm {
             return result;
         }
 
+        template <typename ValueType>
+        bool AssumptionChecker<ValueType>::checkOnSamples(std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption) {
+            bool result = true;
+            std::set<storm::expressions::Variable> vars = std::set<storm::expressions::Variable>({});
+            assumption->gatherVariables(vars);
+            for (auto itr = results.begin(); result && itr != results.end(); ++itr) {
+                std::shared_ptr<storm::expressions::ExpressionManager const> manager = assumption->getManager().getSharedPointer();
+                auto valuation = storm::expressions::SimpleValuation(manager);
+                auto values = (*itr);
+                for (auto var = vars.begin(); result && var != vars.end(); ++var) {
+                    storm::expressions::Variable par = *var;
+                    auto index = std::stoi(par.getName());
+                    valuation.setRationalValue(par, values[index]);
+                }
+                result &= assumption->evaluateAsBool(&valuation);
+            }
+            return result;
+        }
+
         template class AssumptionChecker<storm::RationalFunction>;
     }
 }
\ No newline at end of file
diff --git a/src/storm-pars/analysis/AssumptionChecker.h b/src/storm-pars/analysis/AssumptionChecker.h
index 7bd8cc916..78e209ab2 100644
--- a/src/storm-pars/analysis/AssumptionChecker.h
+++ b/src/storm-pars/analysis/AssumptionChecker.h
@@ -5,9 +5,11 @@
 #ifndef STORM_ASSUMPTIONCHECKER_H
 #define STORM_ASSUMPTIONCHECKER_H
 
-#include <storm/logic/Formula.h>
-#include <storm/models/sparse/Dtmc.h>
+#include "storm/logic/Formula.h"
+#include "storm/models/sparse/Dtmc.h"
 #include "storm/environment/Environment.h"
+#include "storm/storage/expressions/BinaryRelationExpression.h"
+
 
 namespace storm {
     namespace analysis {
@@ -17,16 +19,17 @@ namespace storm {
             AssumptionChecker(std::shared_ptr<storm::logic::Formula const> formula, std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> model, uint_fast64_t numberOfSamples);
 
             bool checkOnSamples(uint_fast64_t val1, uint_fast64_t val2);
+            bool checkOnSamples(std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption);
         private:
             std::shared_ptr<storm::logic::Formula const> formula;
 
-            std::vector<storm::models::sparse::Dtmc<double>> sampleModels;
+//            std::vector<storm::models::sparse::Dtmc<double>> sampleModels;
 
             std::vector<std::vector<double>> results;
 
-            uint_fast64_t numberOfStates;
-
-            storm::storage::BitVector initialStates;
+//            uint_fast64_t numberOfStates;
+//
+//            storm::storage::BitVector initialStates;
         };
     }
 }
diff --git a/src/storm-pars/analysis/AssumptionMaker.cpp b/src/storm-pars/analysis/AssumptionMaker.cpp
index d61b5ef28..db98a3498 100644
--- a/src/storm-pars/analysis/AssumptionMaker.cpp
+++ b/src/storm-pars/analysis/AssumptionMaker.cpp
@@ -13,7 +13,7 @@ namespace storm {
             this->assumptionChecker = assumptionChecker;
             this->expressionManager = std::make_shared<storm::expressions::ExpressionManager>(storm::expressions::ExpressionManager());
             for (uint_fast64_t i = 0; i < this->numberOfStates; ++i) {
-                expressionManager->declareIntegerVariable(std::to_string(i));
+                expressionManager->declareRationalVariable(std::to_string(i));
             }
         }
 
@@ -29,19 +29,14 @@ namespace storm {
                 storm::expressions::Variable var1 = expressionManager->getVariable(std::to_string(critical1));
                 storm::expressions::Variable var2 = expressionManager->getVariable(std::to_string(critical2));
 
-                if (assumptionChecker->checkOnSamples(critical1, critical2)) {
-                    auto latticeCopy = new Lattice(lattice);
-                    std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions;
-                    auto myMap = createAssumptions(var1, var2, latticeCopy, assumptions);
-                    result.insert(myMap.begin(), myMap.end());
-                }
-                if (assumptionChecker->checkOnSamples(critical2, critical1)) {
-                    std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions;
-                    auto myMap = createAssumptions(var2, var1, lattice, assumptions);
-                    result.insert(myMap.begin(), myMap.end());
-                } else {
-                    delete lattice;
-                }
+                auto latticeCopy = new Lattice(lattice);
+                std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions;
+                auto myMap = createAssumptions(var1, var2, latticeCopy, assumptions);
+                result.insert(myMap.begin(), myMap.end());
+
+                std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions2;
+                myMap = createAssumptions(var2, var1, lattice, assumptions2);
+                result.insert(myMap.begin(), myMap.end());
             }
             return result;
         }
@@ -59,31 +54,34 @@ namespace storm {
                 storm::expressions::Variable var1 = expressionManager->getVariable(std::to_string(val1));
                 storm::expressions::Variable var2 = expressionManager->getVariable(std::to_string(val2));
 
-                if (assumptionChecker->checkOnSamples(val1, val2)) {
-                    auto latticeCopy = new Lattice(lattice);
-                    std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptionsCopy = std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>(assumptions);
-                    auto myMap = createAssumptions(var1, var2, latticeCopy, assumptionsCopy);
-                    result.insert(myMap.begin(), myMap.end());
-                }
-
-                if (assumptionChecker->checkOnSamples(val2, val1)) {
-                    auto myMap = createAssumptions(var2, var1, lattice, assumptions);
-                    result.insert(myMap.begin(), myMap.end());
-                } else {
-                    delete lattice;
-                }
+                auto latticeCopy = new Lattice(lattice);
+                std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptionsCopy = std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>(
+                        assumptions);
+                auto myMap = createAssumptions(var1, var2, latticeCopy, assumptionsCopy);
+                result.insert(myMap.begin(), myMap.end());
+
+                myMap = createAssumptions(var2, var1, lattice, assumptions);
+                result.insert(myMap.begin(), myMap.end());
             }
             return result;
         }
 
         template <typename ValueType>
         std::map<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> AssumptionMaker<ValueType>::createAssumptions(storm::expressions::Variable var1, storm::expressions::Variable var2, storm::analysis::Lattice* lattice, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions) {
-            std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption1
-                = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(*expressionManager, var1.getType(),
+            std::map<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> result;
+
+            std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption
+                = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(),
                         var1.getExpression().getBaseExpressionPointer(), var2.getExpression().getBaseExpressionPointer(),
                         storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual));
-            assumptions.insert(assumption1);
-            return (runRecursive(lattice, assumptions));
+            if (assumptionChecker->checkOnSamples(assumption)) {
+                assumptions.insert(assumption);
+                result = (runRecursive(lattice, assumptions));
+            } else {
+                delete lattice;
+            }
+
+            return result;
         }