From 44cde3314c79d6a0dae0b4b7d653e36fb9cfb8a6 Mon Sep 17 00:00:00 2001
From: Jip Spel <jip.spel@cs.rwth-aachen.de>
Date: Thu, 31 Jan 2019 18:34:02 +0100
Subject: [PATCH] Fix checking derivative

---
 src/storm-pars/analysis/MonotonicityChecker.cpp | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/storm-pars/analysis/MonotonicityChecker.cpp b/src/storm-pars/analysis/MonotonicityChecker.cpp
index 21ae0057e..dec5c4b08 100644
--- a/src/storm-pars/analysis/MonotonicityChecker.cpp
+++ b/src/storm-pars/analysis/MonotonicityChecker.cpp
@@ -498,7 +498,7 @@ namespace storm {
                 storm::expressions::Expression exprBounds = manager->boolean(true);
                 auto managervars = manager->getVariables();
                 for (auto var : managervars) {
-                    exprBounds = exprBounds && manager->rational(0) <= var && manager->rational(1) >= var;
+                    exprBounds = exprBounds && manager->rational(0) < var && var < manager->rational(1);
                 }
 
                 auto converter = storm::expressions::RationalFunctionToExpression<ValueType>(manager);
@@ -518,6 +518,10 @@ namespace storm {
                 s.add(exprToCheck2);
                 smtResult = s.check();
                 monDecr = smtResult == storm::solver::SmtSolver::CheckResult::Sat;
+                if (monIncr && monDecr) {
+                    monIncr = false;
+                    monDecr = false;
+                }
             }
             assert (!(monIncr && monDecr) || derivative.isZero());