From 25a915e4ff98f1088f2b7ec90144b400f0cae5d3 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Mon, 30 Jul 2018 23:31:59 +0530 Subject: [PATCH] use simplify() only on BoolRef --- mythril/laser/ethereum/instructions.py | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index ae7ef8fe..0b934a20 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -767,25 +767,25 @@ class Instruction: instr = disassembly.instruction_list[index] # True case - condi = condition if type(condition) == BoolRef else condition != 0 + condi = simplify(condition) if type(condition) == BoolRef else condition != 0 if instr['opcode'] == "JUMPDEST": - if (type(condi) == bool and condi) or (type(condi) == BoolRef and not is_false(simplify(condi))): + if (type(condi) == bool and condi) or (type(condi) == BoolRef and not is_false(condi)): new_state = copy(global_state) new_state.mstate.pc = index new_state.mstate.depth += 1 - new_state.mstate.constraints.append(simplify(condi)) + new_state.mstate.constraints.append(condi) states.append(new_state) else: logging.debug("Pruned unreachable states.") # False case - negated = Not(condition) if type(condition) == BoolRef else condition == 0 + negated = simplify(Not(condition)) if type(condition) == BoolRef else condition == 0 - if (type(negated) == bool and negated) or (type(negated) == BoolRef and not is_false(simplify(negated))): + if (type(negated) == bool and negated) or (type(negated) == BoolRef and not is_false(negated)): new_state = copy(global_state) new_state.mstate.depth += 1 - new_state.mstate.constraints.append(simplify(negated)) + new_state.mstate.constraints.append(negated) states.append(new_state) else: logging.debug("Pruned unreachable states.")