From 05e74735e42e79c3a63954c90d47a018bb61d2cc Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Mon, 28 Jan 2019 16:17:45 +0100 Subject: [PATCH] add edge case handling to model --- mythril/laser/smt/model.py | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/mythril/laser/smt/model.py b/mythril/laser/smt/model.py index 1e758008..a6060d98 100644 --- a/mythril/laser/smt/model.py +++ b/mythril/laser/smt/model.py @@ -27,10 +27,17 @@ class Model: If item is a declaration, then the interpretation is returned """ for internal_model in self.raw: + is_last_model = self.raw.index(internal_model) == len(self.raw) - 1 + try: - return internal_model[item] - except KeyError: + result = internal_model[item] + if result is None: + continue + except IndexError: + if is_last_model: + raise continue + return None def eval(self, expression: z3.ExprRef, model_completion: bool = False): """ Evaluate the expression using this model