laser/instruction: simplify before checking by Z3 is_true()

Z3 is_true() does not automatically consider `expr == expr` to be
true, so `is_true(key_argument == index_argument)` in `sstore_()` will
miss lots of positive conditions and then generate lots of unnecessary
subsequent paths.

Take the following contract for example

```
contract Foo {
    mapping(address => uint) public balances;

    function bar(address _to, uint256 _value) public {
        require(balances[_to] + _value >= balances[_to]);
        balances[_to] += _value;
        balances[_to] += _value;
    }
```

Before this commit,
- 772 nodes/771 edges/8288 states are generated.

After this commit,
- only 237 nodes/236 edges/3204 states are generated.

mythril/laser/ethereum/instructions.py

@@ -929,7 +929,7 @@ class Instruction:
                 key_argument = keccak_function_manager.get_argument(keccak_key)
                 index_argument = keccak_function_manager.get_argument(index)
 
-                if is_true(key_argument == index_argument):
+                if is_true(simplify(key_argument == index_argument)):
                     return self._sstore_helper(
                         copy(global_state),
                         keccak_key,