diff --git a/src/storm/adapters/Z3ExpressionAdapter.cpp b/src/storm/adapters/Z3ExpressionAdapter.cpp
index 8a7f55bf5..bb9afb6f3 100644
--- a/src/storm/adapters/Z3ExpressionAdapter.cpp
+++ b/src/storm/adapters/Z3ExpressionAdapter.cpp
@@ -227,6 +227,9 @@ namespace storm {
                         result = leftResult * rightResult;
                         break;
 					case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Divide:
+                        if (leftResult.is_int() && rightResult.is_int()) {
+                            leftResult = z3::expr(context, Z3_mk_int2real(context, leftResult));
+                        }
                         result = leftResult / rightResult;
                         break;
 					case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Min:
@@ -363,7 +366,7 @@ namespace storm {
 					case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Ceil:{
                         storm::expressions::Variable freshAuxiliaryVariable = manager.declareFreshVariable(manager.getIntegerType(), true);
                         z3::expr ceilVariable = context.int_const(freshAuxiliaryVariable.getName().c_str());
-						additionalAssertions.push_back(z3::expr(context, Z3_mk_int2real(context, ceilVariable)) - 1 <= result && result < z3::expr(context, Z3_mk_int2real(context, ceilVariable)));
+						additionalAssertions.push_back(z3::expr(context, Z3_mk_int2real(context, ceilVariable)) - 1 < result && result <= z3::expr(context, Z3_mk_int2real(context, ceilVariable)));
 						result = ceilVariable;
                         break;
 					}
diff --git a/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp b/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp
index 92ed03c5c..aaafce6cc 100644
--- a/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp
+++ b/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp
@@ -111,7 +111,7 @@ namespace storm {
                         case OperatorType::Divide: newValue = firstOperandEvaluation / secondOperandEvaluation; break;
                         case OperatorType::Power: {
                             if (carl::isInteger(secondOperandEvaluation)) {
-                                std::size_t exponent = carl::toInt<carl::uint>(secondOperandEvaluation);
+                                std::size_t exponent = carl::toInt<carl::sint>(secondOperandEvaluation);
                                 newValue = carl::pow(firstOperandEvaluation, exponent);
                             }
                             break;
diff --git a/src/storm/storage/expressions/ToRationalNumberVisitor.cpp b/src/storm/storage/expressions/ToRationalNumberVisitor.cpp
index c54758b12..24c50e32f 100644
--- a/src/storm/storage/expressions/ToRationalNumberVisitor.cpp
+++ b/src/storm/storage/expressions/ToRationalNumberVisitor.cpp
@@ -76,7 +76,7 @@ namespace storm {
                     break;
                 case BinaryNumericalFunctionExpression::OperatorType::Power:
                     STORM_LOG_THROW(storm::utility::isInteger(secondOperandAsRationalNumber), storm::exceptions::InvalidArgumentException, "Exponent of power operator must be a positive integer.");
-                    exponentAsInteger = storm::utility::convertNumber<carl::uint>(secondOperandAsRationalNumber);
+                    exponentAsInteger = storm::utility::convertNumber<carl::sint>(secondOperandAsRationalNumber);
                     result = storm::utility::pow(firstOperandAsRationalNumber, exponentAsInteger);
                     return result;
                     break;