Try fixing the fp

mythril/analysis/modules/suicide.py

@@ -101,6 +101,7 @@ class SuicideModule(DetectionModule):
                 transaction_sequence=transaction_sequence,
                 gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
             )
+            print(state.mstate.constraints)
             return [issue]
         except UnsatError:
             try:

mythril/laser/ethereum/state/account.py

@@ -193,13 +193,13 @@ class Storage:
     def __getitem__(self, key: BitVec) -> BitVec:
         ite_get = self._ite_region[cast(BitVecFunc, key)]
         array_get = self._array_region[key]
+        print(If(ite_get, ite_get, array_get))
         return If(ite_get, ite_get, array_get)
 
     def __setitem__(self, key: BitVec, value: Any) -> None:
         self._printable_storage[key] = value
         if self._array_condition(key):
             self._array_region[key] = value
-            return
 
         self._ite_region[cast(BitVecFunc, key)] = value
 

mythril/laser/smt/bitvecfunc.py

@@ -67,12 +67,12 @@ def _comparison_helper(
         if operation == z3.ULT:
             operation = operator.lt
         return Bool(z3.BoolVal(operation(a.value, b.value)), annotations=union)
-    if not isinstance(b, BitVecFunc) and a.potential_value:
-        condition = False
-        for value, cond in a.potential_value:
-            if value is not None:
-                condition = Or(condition, And(b == value, cond))
-        return And(condition, operation(a.raw, b.raw))
+    #if not isinstance(b, BitVecFunc) and a.potential_value:
+    #    condition = False
+    #    for value, cond in a.potential_value:
+    #        if value is not None:
+    #            condition = Or(condition, And(b == value, cond))
+    #    return And(condition, operation(a.raw, b.raw))
     if (
         not isinstance(b, BitVecFunc)
         or not a.func_name