Use only one _try constraint call. Cleans up this method. Also add non zero checks to initial constraint (multiplication)

mythril/analysis/modules/integer.py

@@ -74,7 +74,7 @@ def _check_integer_overflow(statespace, state, node):
         expr = op1 * op0
 
     # Check satisfiable
-    constraint = Or(ULT(expr, op0), ULT(expr, op1))
+    constraint = Or(And(ULT(expr, op0), op1 != 0), And(ULT(expr, op1), op0 != 0))
     model = _try_constraints(node.constraints, [constraint])
 
     if model is None:
@@ -106,20 +106,7 @@ def _verify_integer_overflow(statespace, node, expr, state, model, constraint, o
     if len(interesting_usages) == 0:
         return False
 
-    model0, model1 = None, None
-
-    if type(op0) is not int:
-        op0_value = int(str(model.eval(op0, model_completion=True)))
-        model0 = _try_constraints(node.constraints, [op0 != op0_value])
-
-    if type(op1) is not int:
-        op1_value = int(str(model.eval(op1, model_completion=True)))
-        model1 = _try_constraints(node.constraints, [op1 != op1_value])
-
-    if model0 is None and model1 is None:
-        return False
-
-    return True
+    return _try_constraints(node.constraints, [Not(constraint)]) is not None
 
 
 def _try_constraints(constraints, new_constraints):