diff --git a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h
index 609bd8d50..6459be5d1 100644
--- a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h
+++ b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h
@@ -423,13 +423,11 @@ namespace storm {
                         
                         // Then add the constraints for bounds of the integer variables.
                         for (auto const& integerVariable : program.getGlobalIntegerVariables()) {
-                            localSolver->add(integerVariable.getExpressionVariable() >= integerVariable.getLowerBoundExpression());
-                            localSolver->add(integerVariable.getExpressionVariable() <= integerVariable.getUpperBoundExpression());
+                            localSolver->add(integerVariable.getRangeExpression());
                         }
                         for (auto const& module : program.getModules()) {
                             for (auto const& integerVariable : module.getIntegerVariables()) {
-                                localSolver->add(integerVariable.getExpressionVariable() >= integerVariable.getLowerBoundExpression());
-                                localSolver->add(integerVariable.getExpressionVariable() <= integerVariable.getUpperBoundExpression());
+                                localSolver->add(integerVariable.getRangeExpression());
                             }
                         }
                     } else {