fixes github issue #18

src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp

@@ -74,6 +74,7 @@ namespace storm {
                     operandEvaluation = operandSimplified->evaluateAsRational();
                 }
                 
+                bool rationalToInteger = this->getOperatorType() == OperatorType::Floor || this->getOperatorType() == OperatorType::Ceil;
                 if (operandSimplified->hasIntegerType()) {
                     int_fast64_t value = 0;
                     switch (this->getOperatorType()) {
@@ -82,6 +83,15 @@ namespace storm {
                         case OperatorType::Ceil: value = std::ceil(boost::get<int_fast64_t>(operandEvaluation)); break;
                     }
                     return std::shared_ptr<BaseExpression>(new IntegerLiteralExpression(this->getManager(), value));
+                } else if (rationalToInteger) {
+                    int_fast64_t value = 0;
+                    switch (this->getOperatorType()) {
+                        case OperatorType::Floor: value = storm::utility::convertNumber<int_fast64_t>(storm::RationalNumber(carl::floor(boost::get<storm::RationalNumber>(operandEvaluation)))); break;
+                        case OperatorType::Ceil: value = storm::utility::convertNumber<int_fast64_t>(storm::RationalNumber(carl::ceil(boost::get<storm::RationalNumber>(operandEvaluation)))); break;
+                        default:
+                            STORM_LOG_ASSERT(false, "Unexpected rational to integer conversion.");
+                    }
+                    return std::shared_ptr<BaseExpression>(new IntegerLiteralExpression(this->getManager(), value));
                 } else {
                     storm::RationalNumber value = storm::utility::zero<storm::RationalNumber>();
                     switch (this->getOperatorType()) {

src/storm/utility/constants.cpp

@@ -325,6 +325,11 @@ namespace storm {
             return carl::toInt<carl::uint>(number);
         }
 
+        template<>
+        int_fast64_t convertNumber(ClnRationalNumber const& number) {
+            return carl::toInt<carl::sint>(number);
+        }
+
         template<>
         ClnRationalNumber convertNumber(double const& number) {
             return carl::rationalize<ClnRationalNumber>(number);
@@ -517,6 +522,11 @@ namespace storm {
             return carl::toInt<carl::uint>(number);
         }
 
+        template<>
+        int_fast64_t convertNumber(GmpRationalNumber const& number){
+            return carl::toInt<carl::sint>(number);
+        }
+
         template<>
         GmpRationalNumber convertNumber(double const& number){
             return carl::rationalize<GmpRationalNumber>(number);