Change interger.py to check for specific overflow in overflow.solc for debugging purposes

mythril/analysis/modules/integer.py

@@ -71,14 +71,37 @@ def _check_integer_overflow(statespace, state, node):
     else:
         expr = op0 * op1
 
+    if str(op1) != 'calldata_Over_32 + 4':
+        return issues
+
     # Check satisfiable
-    constraint = UGT(expr, MAX_UINT)
+    constraint = UGT(op1, MAX_UINT - 1)
+    model = _try_constraints(node.constraints, [constraint])
+
+    if model is None:
+        logging.debug("[INTEGER_OVERFLOW] no model found")
+        return issues
+
+    constraint = UGT(op0, MAX_UINT - 1)
     model = _try_constraints(node.constraints, [constraint])
 
     if model is None:
         logging.debug("[INTEGER_OVERFLOW] no model found")
         return issues
 
+    constraint = ULT(op0 + op1, op0)
+    model = _try_constraints(node.constraints, [constraint])
+
+    if model is None:
+        logging.debug("[INTEGER_OVERFLOW] no model found")
+        return issues
+
+    print(op0)
+    print("::")
+    print(op1)
+    print("::")
+    print(node.constraints)
+
     if not _verify_integer_overflow(statespace, node, expr, state, model, constraint, op0, op1):
         return issues
 

mythril/analysis/solver.py

@@ -4,7 +4,7 @@ from mythril.exceptions import UnsatError
 
 def get_model(constraints):
     s = Solver()
-    s.set("timeout", 2000)
+    s.set("timeout", 40000)
 
     for constraint in constraints:
         s.add(constraint)