From 09a5c44c6e55f16b7ecdb9d3a99920811d70bbe8 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Thu, 24 Jan 2019 13:58:47 +0100
Subject: [PATCH] Fixed usage of denominatorAsNumber

---
 src/storm/analysis/GraphConditions.cpp | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/storm/analysis/GraphConditions.cpp b/src/storm/analysis/GraphConditions.cpp
index 663bf2b52..c11fccb0b 100644
--- a/src/storm/analysis/GraphConditions.cpp
+++ b/src/storm/analysis/GraphConditions.cpp
@@ -38,9 +38,10 @@ namespace storm {
                     auto const& transitionVars = entry.gatherVariables();
                     variableSet.insert(transitionVars.begin(), transitionVars.end());
                     if (entry.denominator().isConstant()) {
-                        if (entry.denominatorAsNumber() > 0) {
+                        assert(entry.denominator().constantPart() != 0);
+                        if (entry.denominator().constantPart() > 0) {
                             wellformedConstraintSet.emplace(entry.nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ);
-                        } else if (entry.denominatorAsNumber() < 0) {
+                        } else if (entry.denominator().constantPart() < 0) {
                             wellformedConstraintSet.emplace(entry.nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ);
                         } else {
                             assert(false); // Should fail before.
@@ -117,9 +118,10 @@ namespace storm {
                     for (auto const& entry : rewModelEntry.second.getTransitionRewardMatrix()) {
                         if(!entry.getValue().isConstant()) {
                             if (entry.getValue().denominator().isConstant()) {
-                                if (entry.getValue().denominatorAsNumber() > 0) {
+                                assert(entry.getValue().denominator().constantPart() != 0);
+                                if (entry.getValue().denominator().constantPart() > 0) {
                                     wellformedConstraintSet.emplace(entry.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ);
-                                } else if (entry.getValue().denominatorAsNumber() < 0) {
+                                } else if (entry.getValue().denominator().constantPart() < 0) {
                                     wellformedConstraintSet.emplace(entry.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ);
                                 } else {
                                     assert(false); // Should fail before.