Chenfeng Wei

Overall, it looks good. Just some small comments: 1. As said, for each tuple comment, we can obtain the type info from `typeDescriptions` nodes. However, I am also okay with...

Probably a bug. Might due to the name issue I am trying to fix #1697. Will investigate. Thanks for reporting this, @fbrausse !

> I am not entirely sure why so much string manipulation is necessary to be performed by goto_coveraget. Couldn't the expressions be manipulated instead? The main idea is to add...

I think the `from_expr` issue could be addressed in another PR... The main reason is that the current multi-property is also highly relied on from_expr. So if we do not...

> I think the `from_expr` issue could be addressed in another PR... The main reason is that the current multi-property is also highly relied on from_expr. So if we do...

Thanks a lot, @fbrausse !

> @ChenfengWei0: Can I ask you whether you had a chance to address Franz's comments? I will resolve the issues after finishing the solidity mapping.

Changed as suggested. Thanks for the advice, @lucasccordeiro !

`--multi-property --keep-verified-claims` ```sh Slicing time: 0.001s (removed 14 assignments) No solver specified; defaulting to Boolector Encoding remaining VCC(s) using bit-vector/floating-point arithmetic Encoding to solver time: 0.001s Solving claim 'a[(signed long...

@JacobYiu You might also want to consider the tuple used as multiple return value. E.g., ```solidity function returnVars() internal pure returns(uint,uint,uint) { uint var1 = 1; uint var2 = 2;...