diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
index f807f1db3..77fd60108 100644
--- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
+++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
@@ -1,8 +1,12 @@
 #include "DFTASFChecker.h"
 #include "SmtConstraint.cpp"
 #include <string>
+
 #include "storm/utility/file.h"
 #include "storm/utility/bitoperations.h"
+#include "storm/solver/SmtSolver.h"
+#include "storm/storage/expressions/ExpressionManager.h"
+#include "storm/storage/expressions/Type.h"
 #include "storm/exceptions/NotImplementedException.h"
 #include "storm/exceptions/NotSupportedException.h"
 
@@ -429,5 +433,30 @@ namespace storm {
             stream << "(check-sat)" << std::endl;
             storm::utility::closeFile(stream);
         }
+
+        void DFTASFChecker::toSolver() {
+            std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
+            std::unique_ptr<storm::solver::SmtSolver> solver = storm::utility::solver::SmtSolverFactory().create(
+                    *manager);
+            for (auto const &timeVarEntry : timePointVariables) {
+                manager->declareIntegerVariable(varNames[timeVarEntry.second]);
+            }
+            for (auto const &claimVarEntry : claimVariables) {
+                manager->declareIntegerVariable(varNames[claimVarEntry.second]);
+            }
+            for (auto const &markovianVarEntry : markovianVariables) {
+                manager->declareBooleanVariable(varNames[markovianVarEntry.second]);
+            }
+            if (!tmpTimePointVariables.empty()) {
+                for (auto const &tmpVar : tmpTimePointVariables) {
+                    manager->declareIntegerVariable(varNames[tmpVar]);
+                }
+            }
+            for (auto const &constraint : constraints) {
+                solver->add(constraint->toExpression(varNames, manager));
+            }
+
+            //TODO Add porperties to check
+        }
     }
 }
diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.h b/src/storm-dft/modelchecker/dft/DFTASFChecker.h
index 3df55519e..f202b40e7 100644
--- a/src/storm-dft/modelchecker/dft/DFTASFChecker.h
+++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.h
@@ -6,7 +6,7 @@
 
 #include "SmtConstraint.h"
 #include "storm-dft/storage/dft/DFT.h"
-
+#include "storm/utility/solver.h"
 
 namespace storm {
     namespace modelchecker {
@@ -29,14 +29,12 @@ namespace storm {
             using ValueType = double;
         public:
             DFTASFChecker(storm::storage::DFT<ValueType> const&);
-
             /**
              * Generate general variables and constraints for the DFT and store them in the corresponding maps and vectors
              *
              */
             void convert();
             void toFile(std::string const&);
-
             void toSolver();
             
         private:
diff --git a/src/storm-dft/modelchecker/dft/SmtConstraint.cpp b/src/storm-dft/modelchecker/dft/SmtConstraint.cpp
index 232431c21..bfec8b438 100644
--- a/src/storm-dft/modelchecker/dft/SmtConstraint.cpp
+++ b/src/storm-dft/modelchecker/dft/SmtConstraint.cpp
@@ -34,6 +34,11 @@ namespace storm {
                 return sstr.str();
             }
 
+            storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
+                                                        std::shared_ptr<storm::expressions::ExpressionManager> manager) const override {
+                //TODO
+            }
+
         private:
             uint64_t varIndex;
             std::vector<uint64_t> varIndices;
@@ -69,6 +74,11 @@ namespace storm {
                 return sstr.str();
             }
 
+            storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
+                                                        std::shared_ptr<storm::expressions::ExpressionManager> manager) const override {
+                //TODO
+            }
+
         private:
             uint64_t varIndex;
             std::vector<uint64_t> varIndices;
@@ -93,6 +103,11 @@ namespace storm {
                 return sstr.str();
             }
 
+            storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
+                                                        std::shared_ptr<storm::expressions::ExpressionManager> manager) const override {
+                //TODO
+            }
+
         private:
             uint64_t varIndex;
             uint64_t upperBound;
@@ -122,6 +137,11 @@ namespace storm {
                 return sstr.str();
             }
 
+            storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
+                                                        std::shared_ptr<storm::expressions::ExpressionManager> manager) const override {
+                //TODO
+            }
+
         private:
             std::vector<std::shared_ptr<SmtConstraint>> constraints;
 
@@ -150,6 +170,11 @@ namespace storm {
                 return sstr.str();
             }
 
+            storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
+                                                        std::shared_ptr<storm::expressions::ExpressionManager> manager) const override {
+                //TODO
+            }
+
         private:
             std::vector<std::shared_ptr<SmtConstraint>> constraints;
 
@@ -167,6 +192,11 @@ namespace storm {
                 return sstr.str();
             }
 
+            storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
+                                                        std::shared_ptr<storm::expressions::ExpressionManager> manager) const override {
+                //TODO
+            }
+
         private:
             std::shared_ptr<SmtConstraint> lhs;
             std::shared_ptr<SmtConstraint> rhs;
@@ -184,6 +214,11 @@ namespace storm {
                 return sstr.str();
             }
 
+            storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
+                                                        std::shared_ptr<storm::expressions::ExpressionManager> manager) const override {
+                //TODO
+            }
+
         private:
             std::shared_ptr<SmtConstraint> lhs;
             std::shared_ptr<SmtConstraint> rhs;
@@ -204,6 +239,11 @@ namespace storm {
                 return sstr.str();
             }
 
+            storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
+                                                        std::shared_ptr<storm::expressions::ExpressionManager> manager) const override {
+                //TODO
+            }
+
         private:
             bool value;
         };
@@ -228,6 +268,11 @@ namespace storm {
                 return sstr.str();
             }
 
+            storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
+                                                        std::shared_ptr<storm::expressions::ExpressionManager> manager) const override {
+                //TODO
+            }
+
         private:
             uint64_t varIndex;
             bool value;
@@ -249,6 +294,11 @@ namespace storm {
                 return sstr.str();
             }
 
+            storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
+                                                        std::shared_ptr<storm::expressions::ExpressionManager> manager) const override {
+                //TODO
+            }
+
         private:
             uint64_t varIndex;
             uint64_t value;
@@ -270,6 +320,11 @@ namespace storm {
                 return sstr.str();
             }
 
+            storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
+                                                        std::shared_ptr<storm::expressions::ExpressionManager> manager) const override {
+                //TODO
+            }
+
         private:
             uint64_t varIndex;
             uint64_t value;
@@ -290,6 +345,11 @@ namespace storm {
                 return sstr.str();
             }
 
+            storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
+                                                        std::shared_ptr<storm::expressions::ExpressionManager> manager) const override {
+                //TODO
+            }
+
         private:
             uint64_t varIndex;
             uint64_t value;
@@ -308,6 +368,11 @@ namespace storm {
                 return "(= " + varNames.at(var1Index) + " " + varNames.at(var2Index) + ")";
             }
 
+            storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
+                                                        std::shared_ptr<storm::expressions::ExpressionManager> manager) const override {
+                //TODO
+            }
+
         private:
             uint64_t var1Index;
             uint64_t var2Index;
@@ -326,6 +391,11 @@ namespace storm {
                 return "(< " + varNames.at(var1Index) + " " + varNames.at(var2Index) + ")";
             }
 
+            storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
+                                                        std::shared_ptr<storm::expressions::ExpressionManager> manager) const override {
+                //TODO
+            }
+
         private:
             uint64_t var1Index;
             uint64_t var2Index;
@@ -355,6 +425,11 @@ namespace storm {
                 return sstr.str();
             }
 
+            storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
+                                                        std::shared_ptr<storm::expressions::ExpressionManager> manager) const override {
+                //TODO
+            }
+
         private:
             std::vector<uint64_t> varIndices;
         };
@@ -378,6 +453,11 @@ namespace storm {
                 return sstr.str();
             }
 
+            storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
+                                                        std::shared_ptr<storm::expressions::ExpressionManager> manager) const override {
+                //TODO
+            }
+
         private:
             std::vector<uint64_t> varIndices;
         };
@@ -397,6 +477,11 @@ namespace storm {
                 return sstr.str();
             }
 
+            storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
+                                                        std::shared_ptr<storm::expressions::ExpressionManager> manager) const override {
+                //TODO
+            }
+
         private:
             std::shared_ptr<SmtConstraint> ifConstraint;
             std::shared_ptr<SmtConstraint> thenConstraint;
diff --git a/src/storm-dft/modelchecker/dft/SmtConstraint.h b/src/storm-dft/modelchecker/dft/SmtConstraint.h
index ef5f6e073..2487f9dfd 100644
--- a/src/storm-dft/modelchecker/dft/SmtConstraint.h
+++ b/src/storm-dft/modelchecker/dft/SmtConstraint.h
@@ -1,4 +1,5 @@
 #include <string>
+#include <storm/storage/expressions/Expression.h>
 
 namespace storm {
     namespace modelchecker {
@@ -9,6 +10,9 @@ namespace storm {
 
             virtual std::string toSmtlib2(std::vector<std::string> const &varNames) const = 0;
 
+            virtual storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
+                                                                std::shared_ptr<storm::expressions::ExpressionManager> manager) const = 0;
+
             virtual std::string description() const {
                 return descript;
             }