diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h
index 250083ea7..fcb0aff94 100644
--- a/src/counterexamples/SMTMinimalCommandSetGenerator.h
+++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h
@@ -1693,7 +1693,7 @@ namespace storm {
                     storm::models::Mdp<T> subMdp = labeledMdp.restrictChoiceLabels(commandSet);
                     storm::modelchecker::SparseMdpPrctlModelChecker<T> modelchecker(subMdp);
                     LOG4CPLUS_DEBUG(logger, "Invoking model checker.");
-                    std::vector<T> result = modelchecker.checkUntil(false, phiStates, psiStates, false).first;
+                    std::vector<T> result = modelchecker.computeUntilProbabilitiesHelper(false, phiStates, psiStates, false)
                     LOG4CPLUS_DEBUG(logger, "Computed model checking results.");
                     totalModelCheckingTime += std::chrono::high_resolution_clock::now() - modelCheckingClock;
 
diff --git a/src/logic/BinaryPathFormula.cpp b/src/logic/BinaryPathFormula.cpp
index 046d53803..adfac9686 100644
--- a/src/logic/BinaryPathFormula.cpp
+++ b/src/logic/BinaryPathFormula.cpp
@@ -44,10 +44,12 @@ namespace storm {
         
         void BinaryPathFormula::gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const {
             this->getLeftSubformula().gatherAtomicExpressionFormulas(atomicExpressionFormulas);
+            this->getLeftSubformula().gatherAtomicExpressionFormulas(atomicExpressionFormulas);
         }
         
         void BinaryPathFormula::gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const {
             this->getLeftSubformula().gatherAtomicLabelFormulas(atomicLabelFormulas);
+            this->getRightSubformula().gatherAtomicLabelFormulas(atomicLabelFormulas);
         }
     }
 }
\ No newline at end of file
diff --git a/src/logic/BinaryStateFormula.cpp b/src/logic/BinaryStateFormula.cpp
index e8557651b..fb9a7560e 100644
--- a/src/logic/BinaryStateFormula.cpp
+++ b/src/logic/BinaryStateFormula.cpp
@@ -44,10 +44,12 @@ namespace storm {
         
         void BinaryStateFormula::gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const {
             this->getLeftSubformula().gatherAtomicExpressionFormulas(atomicExpressionFormulas);
+            this->getRightSubformula().gatherAtomicExpressionFormulas(atomicExpressionFormulas);
         }
         
         void BinaryStateFormula::gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const {
             this->getLeftSubformula().gatherAtomicLabelFormulas(atomicLabelFormulas);
+            this->getRightSubformula().gatherAtomicLabelFormulas(atomicLabelFormulas);
         }
     }
 }
\ No newline at end of file
diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
index a24dfcc06..a3a7a9c08 100644
--- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
+++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
@@ -7,6 +7,11 @@
 #include "src/solver/NondeterministicLinearEquationSolver.h"
 
 namespace storm {
+    namespace counterexamples {
+        template<typename ValueType>
+        class SMTMinimalCommandSetGenerator;
+    }
+    
     namespace modelchecker {
         
         // Forward-declare other model checkers to make them friend classes.
@@ -17,6 +22,7 @@ namespace storm {
         class SparseMdpPrctlModelChecker : public AbstractModelChecker {
         public:
             friend class SparseMarkovAutomatonCslModelChecker<ValueType>;
+            friend class counterexamples::SMTMinimalCommandSetGenerator<ValueType>;
             
             explicit SparseMdpPrctlModelChecker(storm::models::Mdp<ValueType> const& model);
             explicit SparseMdpPrctlModelChecker(storm::models::Mdp<ValueType> const& model, std::shared_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>> nondeterministicLinearEquationSolver);
diff --git a/src/utility/cli.h b/src/utility/cli.h
index 73ff738ee..de987e365 100644
--- a/src/utility/cli.h
+++ b/src/utility/cli.h
@@ -274,9 +274,8 @@ namespace storm {
                 typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
                 if (formula) {
                     options = storm::builder::ExplicitPrismModelBuilder<double>::Options(*formula.get());
-                } else {
-                    options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString());
                 }
+                options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString());
                 
                 // Then, build the model from the symbolic description.
                 result = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);