From daae260d6ae3e75b40b632f55bce0539a91bd995 Mon Sep 17 00:00:00 2001
From: Filip Macak <filip.macak1999@gmail.com>
Date: Fri, 6 Dec 2024 21:15:52 +0100
Subject: [PATCH] Fixed assert in SMG model checker

---
 .../smg/modelchecker/helper/SparseSmgRpatlHelper.cpp     | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/payntbind/src/synthesis/smg/modelchecker/helper/SparseSmgRpatlHelper.cpp b/payntbind/src/synthesis/smg/modelchecker/helper/SparseSmgRpatlHelper.cpp
index a7356c54..da626a5b 100644
--- a/payntbind/src/synthesis/smg/modelchecker/helper/SparseSmgRpatlHelper.cpp
+++ b/payntbind/src/synthesis/smg/modelchecker/helper/SparseSmgRpatlHelper.cpp
@@ -30,8 +30,8 @@ namespace synthesis {
         }
     }
 
-    bool epsilonGreaterOrEqual(double x, double y, double eps=1e-8) {
-        return (x>=y) || (abs(x - y) <= eps);
+    bool epsilonGreaterOrEqual(double x, double y, double eps=1e-6) {
+        return (x>=y) || (fabs(x - y) <= eps);
     }
 
     template<typename ValueType>
@@ -178,8 +178,11 @@ namespace synthesis {
                     }
                 }
 
-                // double check if all states have a choice
+                //double check if all states have a choice
                 for (uint64_t state = 0; state < stateCount; state++) {
+                    if (!relevantStates.get(state)) {
+                        continue;
+                    }
                     assert(optimalChoiceSet.get(state));
                 }