diff --git a/src/core/counterexample.cpp b/src/core/counterexample.cpp
index e92445c..b3eb054 100644
--- a/src/core/counterexample.cpp
+++ b/src/core/counterexample.cpp
@@ -23,7 +23,9 @@ void define_counterexamples(py::module& m) {
             .def_readonly("analysis_time", &CexGeneratorStats::analysisTime)
             .def_readonly("setup_time", &CexGeneratorStats::setupTime)
             .def_readonly("model_checking_time", &CexGeneratorStats::modelCheckingTime)
-            .def_readonly("solver_time", &CexGeneratorStats::solverTime);
+            .def_readonly("solver_time", &CexGeneratorStats::solverTime)
+            .def_readonly("cut_time", &CexGeneratorStats::cutTime)
+            .def_readonly("iterations", &CexGeneratorStats::iterations);
 
     using CexGeneratorOptions =  SMTMinimalLabelSetGenerator<double>::Options;
             py::class_<CexGeneratorOptions>(m, "SMTCounterExampleGeneratorOptions", "Options for highlevel counterexample generation")
@@ -31,10 +33,11 @@ void define_counterexamples(py::module& m) {
                     .def_readwrite("check_threshold_feasible", &CexGeneratorOptions::checkThresholdFeasible)
                     .def_readwrite("encode_reachability", &CexGeneratorOptions::encodeReachability)
                     .def_readwrite("silent", &CexGeneratorOptions::silent)
+                    .def_readwrite("add_backward_implication_cuts", &CexGeneratorOptions::addBackwardImplicationCuts)
                     .def_readwrite("use_dynamic_constraints", &CexGeneratorOptions::useDynamicConstraints)
                     .def_readwrite("maximum_counterexamples", &CexGeneratorOptions::maximumCounterexamples)
                     .def_readwrite("continue_after_first_counterexample",  &CexGeneratorOptions::continueAfterFirstCounterexampleUntil)
-
+                    .def_readwrite("maximum_iterations_after_counterexample", &CexGeneratorOptions::maximumExtraIterations)
             ;
             py::class_<SMTMinimalLabelSetGenerator<double>>(m, "SMTCounterExampleGenerator", "Highlevel Counterexample Generator with SMT as backend").
                 def_static("precompute", &SMTMinimalLabelSetGenerator<double>::precompute, "Precompute input for counterexample generation", py::arg("env"), py::arg("symbolic_model"), py::arg("model"), py::arg("formula")).
diff --git a/src/core/environment.cpp b/src/core/environment.cpp
index 23ad447..6e6f8f8 100644
--- a/src/core/environment.cpp
+++ b/src/core/environment.cpp
@@ -1,10 +1,33 @@
 #include "environment.h"
 #include "src/helpers.h"
 #include "storm/environment/Environment.h"
+#include "storm/environment/solver/SolverEnvironment.h"
+#include "storm/environment/solver/EigenSolverEnvironment.h"
+#include "storm/environment/solver/GmmxxSolverEnvironment.h"
+#include "storm/environment/solver/GameSolverEnvironment.h"
+#include "storm/environment/solver/NativeSolverEnvironment.h"
+#include "storm/environment/solver/TopologicalSolverEnvironment.h"
+#include "storm/environment/solver/MultiplierEnvironment.h"
+#include "storm/environment/solver/MinMaxSolverEnvironment.h"
 
 void define_environment(py::module& m) {
+    py::enum_<storm::solver::EquationSolverType>(m, "EquationSolverType", "Solver type for equation systems")
+        .value("native", storm::solver::EquationSolverType::Native)
+        .value("eigen", storm::solver::EquationSolverType::Eigen)
+        .value("elimination", storm::solver::EquationSolverType::Elimination)
+        .value("gmmxx", storm::solver::EquationSolverType::Gmmxx)
+        .value("topological", storm::solver::EquationSolverType::Topological)
+    ;
+
     py::class_<storm::Environment>(m, "Environment", "Environment")
         .def(py::init<>(), "Construct default environment")
+        .def_property_readonly("solver_environment", [](storm::Environment& env) {return env.solver();}, "solver part of environment")
     ;
+
+    py::class_<storm::SolverEnvironment>(m, "SolverEnvironment", "Environment for solvers")
+        .def("set_force_sound", &storm::SolverEnvironment::setForceSoundness, "force soundness", py::arg("new_value") = true)
+        .def("set_linear_equation_solver_type", &storm::SolverEnvironment::setLinearEquationSolverType, "set solver type to use", py::arg("new_value"), py::arg("set_from_default") = false)
+    ;
+
 }