diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h
index ab578f1f4..0e552c649 100644
--- a/src/counterexamples/SMTMinimalCommandSetGenerator.h
+++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h
@@ -356,6 +356,7 @@ namespace storm {
                 // FIXME: Include synchronisation cuts.
                 // FIXME: Fix backward cuts in the presence of synchronizing actions.
                 std::map<uint_fast64_t, std::set<uint_fast64_t>> precedingLabels;
+                std::set<uint_fast64_t> hasSynchronizingPredecessor;
 
                 // Get some data from the MDP for convenient access.
                 storm::storage::SparseMatrix<T> const& transitionMatrix = labeledMdp.getTransitionMatrix();
@@ -377,6 +378,11 @@ namespace storm {
                                 }
                                 
                                 if (choiceTargetsCurrentState) {
+                                    if (choiceLabeling.at(predecessorChoice).size() > 1) {
+                                        for (auto label : choiceLabeling.at(currentChoice)) {
+                                            hasSynchronizingPredecessor.insert(label);
+                                        }
+                                    }
                                     for (auto labelToAdd : choiceLabeling[predecessorChoice]) {
                                         for (auto labelForWhichToAdd : choiceLabeling[currentChoice]) {
                                             precedingLabels[labelForWhichToAdd].insert(labelToAdd);
diff --git a/src/parser/prismparser/PrismGrammar.cpp b/src/parser/prismparser/PrismGrammar.cpp
index a6d7a62a5..90b590341 100644
--- a/src/parser/prismparser/PrismGrammar.cpp
+++ b/src/parser/prismparser/PrismGrammar.cpp
@@ -179,7 +179,7 @@ namespace storm {
                 assignmentDefinition.name("assignment");
                 assignmentDefinitionList = assignmentDefinition(qi::_r1, qi::_r2) % "&";
                 assignmentDefinitionList.name("assignment list");
-                updateDefinition = (ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(":")[phoenix::clear(phoenix::ref(this->state->assignedBooleanVariables_)), phoenix::clear(phoenix::ref(this->state->assignedIntegerVariables_))] > assignmentDefinitionList(qi::_a, qi::_b))[qi::_val = phoenix::bind(&PrismGrammar::createUpdate, this, qi::_1, qi::_a, qi::_b)];
+                updateDefinition = ((ConstDoubleExpressionGrammar::instance(this->state) | qi::attr(phoenix::construct<std::shared_ptr<BaseExpression>>(phoenix::new_<storm::ir::expressions::DoubleLiteralExpression>(1)))) > qi::lit(":")[phoenix::clear(phoenix::ref(this->state->assignedBooleanVariables_)), phoenix::clear(phoenix::ref(this->state->assignedIntegerVariables_))] > assignmentDefinitionList(qi::_a, qi::_b))[qi::_val = phoenix::bind(&PrismGrammar::createUpdate, this, qi::_1, qi::_a, qi::_b)];
                 updateDefinition.name("update");
                 updateListDefinition = +updateDefinition % "+";
                 updateListDefinition.name("update list");
diff --git a/src/storm.cpp b/src/storm.cpp
index 943455fc1..e68fc4b9e 100644
--- a/src/storm.cpp
+++ b/src/storm.cpp
@@ -338,28 +338,32 @@ int main(const int argc, const char* argv[]) {
 			model->printModelInformationToStream(std::cout);
 
             // Enable the following lines to test the MinimalLabelSetGenerator.
-            if (model->getType() == storm::models::MDP) {
-                std::shared_ptr<storm::models::Mdp<double>> labeledMdp = model->as<storm::models::Mdp<double>>();
-                storm::storage::BitVector const& finishedStates = labeledMdp->getLabeledStates("finished");
-                storm::storage::BitVector const& allCoinsEqual1States = labeledMdp->getLabeledStates("all_coins_equal_1");
-                storm::storage::BitVector targetStates = finishedStates & allCoinsEqual1States;
-                std::set<uint_fast64_t> labels = storm::counterexamples::MILPMinimalLabelSetGenerator<double>::getMinimalLabelSet(*labeledMdp, storm::storage::BitVector(labeledMdp->getNumberOfStates(), true), targetStates, 0.4, true, true);
-                
-                std::cout << "Found solution with " << labels.size() << " commands." << std::endl;
-                for (uint_fast64_t label : labels) {
-                    std::cout << label << ", ";
-                }
-                std::cout << std::endl;
-            }
-            
-            // Enable the following lines to test the SMTMinimalCommandSetGenerator.
 //            if (model->getType() == storm::models::MDP) {
 //                std::shared_ptr<storm::models::Mdp<double>> labeledMdp = model->as<storm::models::Mdp<double>>();
 //                storm::storage::BitVector const& finishedStates = labeledMdp->getLabeledStates("finished");
 //                storm::storage::BitVector const& allCoinsEqual1States = labeledMdp->getLabeledStates("all_coins_equal_1");
 //                storm::storage::BitVector targetStates = finishedStates & allCoinsEqual1States;
-//                std::set<uint_fast64_t> labels = storm::counterexamples::SMTMinimalCommandSetGenerator<double>::getMinimalCommandSet(program, constants, *labeledMdp, storm::storage::BitVector(labeledMdp->getNumberOfStates(), true), targetStates, 0.4, true);
+//                std::set<uint_fast64_t> labels = storm::counterexamples::MILPMinimalLabelSetGenerator<double>::getMinimalLabelSet(*labeledMdp, storm::storage::BitVector(labeledMdp->getNumberOfStates(), true), targetStates, 0.4, true, true);
+//                
+//                std::cout << "Found solution with " << labels.size() << " commands." << std::endl;
+//                for (uint_fast64_t label : labels) {
+//                    std::cout << label << ", ";
+//                }
+//                std::cout << std::endl;
 //            }
+            
+            // Enable the following lines to test the SMTMinimalCommandSetGenerator.
+            if (model->getType() == storm::models::MDP) {
+                std::shared_ptr<storm::models::Mdp<double>> labeledMdp = model->as<storm::models::Mdp<double>>();
+//                storm::storage::BitVector const& finishedStates = labeledMdp->getLabeledStates("finished");
+//                storm::storage::BitVector const& allCoinsEqual1States = labeledMdp->getLabeledStates("all_coins_equal_1");
+//                storm::storage::BitVector targetStates = finishedStates & allCoinsEqual1States;
+//                std::set<uint_fast64_t> labels = storm::counterexamples::SMTMinimalCommandSetGenerator<double>::getMinimalCommandSet(program, constants, *labeledMdp, storm::storage::BitVector(labeledMdp->getNumberOfStates(), true), targetStates, 0.4, true);
+                
+                storm::storage::BitVector const& collisionStates = labeledMdp->getLabeledStates("collision_max_backoff");
+                storm::storage::BitVector const& deliveredStates = labeledMdp->getLabeledStates("all_delivered");
+                std::set<uint_fast64_t> labels = storm::counterexamples::MILPMinimalLabelSetGenerator<double>::getMinimalLabelSet(*labeledMdp, ~collisionStates, deliveredStates, 0.5, true, true);
+            }
 		}
 
         // Perform clean-up and terminate.