diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h
index 19b165f0a..fd619e18d 100644
--- a/src/counterexamples/MILPMinimalLabelSetGenerator.h
+++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h
@@ -180,6 +180,12 @@ namespace storm {
                 // Enable the following line to only print the output of Gurobi if the debug flag is set.
                 // int error = error = GRBsetintparam(env, "OutputFlag", storm::settings::Settings::getInstance()->isSet("debug") ? 1 : 0);
                 int error = error = GRBsetintparam(env, "OutputFlag", 1);
+                
+                // Enable the following line to restrict Gurobi to one thread only.
+                // error = error = GRBsetintparam(env, "Threads", 1);
+                
+                // Enable the following line to force Gurobi to be as precise about the binary variables as required by the given precision option.
+                error = GRBsetdblparam(env, "IntFeasTol", storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
             }
             
             /*!
diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h
index c2aa105ce..8338846e0 100644
--- a/src/counterexamples/SMTMinimalCommandSetGenerator.h
+++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h
@@ -1164,6 +1164,8 @@ namespace storm {
                     }
                 } while (!done);
                 
+                std::cout << "Checked " << iterations << " models in total out of which " << zeroProbabilityCount << " could not reach the target states." << std::endl;
+                
                 // (9) Return the resulting command set after undefining the constants.
                 storm::utility::ir::undefineUndefinedConstants(program);