From ede791cff7893962958cba00d678fbf0e5933e52 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 6 Apr 2018 15:59:02 +0200
Subject: [PATCH] fixing bug in Z3 LP solver

---
 src/storm/solver/Z3LpSolver.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/storm/solver/Z3LpSolver.cpp b/src/storm/solver/Z3LpSolver.cpp
index 0c4bbc3e8..bd37e1baa 100644
--- a/src/storm/solver/Z3LpSolver.cpp
+++ b/src/storm/solver/Z3LpSolver.cpp
@@ -127,7 +127,7 @@ namespace storm {
         template<typename ValueType>
         storm::expressions::Variable Z3LpSolver<ValueType>::addBinaryVariable(std::string const& name, ValueType objectiveFunctionCoefficient) {
             storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getIntegerType());
-            solver->add(expressionAdapter->translateExpression((newVariable.getExpression() >= this->manager->rational(storm::utility::one<storm::RationalNumber>())) && (newVariable.getExpression() <= this->manager->rational(storm::utility::one<storm::RationalNumber>()))));
+            solver->add(expressionAdapter->translateExpression((newVariable.getExpression() >= this->manager->rational(storm::utility::zero<storm::RationalNumber>())) && (newVariable.getExpression() <= this->manager->rational(storm::utility::one<storm::RationalNumber>()))));
             optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable;
             return newVariable;
         }