[SMTChecker] Stack overflow due to nested SMT expressions in Gnosis safe contract

[bshastry]

Moved from https://github.com/ethereum/solidity/pull/10961

This test https://gist.github.com/bshastry/395f7484727b9f42060d54d26dc9caec

when copied to test/libsolidity/syntaxTests/multiSource/gnosisSafe.sol

and invoked like so

$ isoltest -t syntaxTests/multiSouce/gnosisSafe

leads to a SIGKILL because of running out of stack memory. The associated stack trace may be found here: https://gist.github.com/bshastry/c0752f16c3952e8a1fcbe0813c033318#file-smt_segfault_gnosissafe_stacktrace-txt-L759

Also see https://github.com/ethereum/solidity/pull/10961#issuecomment-779112262

[cameel]

@bshastry @leonardoalt I have reopened #10961 to push a smaller repro (~600 lines). See https://github.com/ethereum/solidity/pull/10961#issuecomment-829666764 for details.

Not sure the PR is worth keeping open so feel free to close it again and just move the repro to a gist. Overall my opinion is that it's not really a bug and more like a performance problem when running on a contract this size. In my opinion it could be a good candidate for a SMT performance test and a benchmark for optimizations.

[leonardoalt]

@cameel yea that's also how I'm seeing this. I have another pretty heavy benchmark from the Circles contract, gets killed even with abstractions and 32gb of ram. I'll collect these somewhere as performance tests. It's a really good goal to try to not get those killed via abstractions. However, at some point we can't abstract more and it ultimately depends on the solver. I'm also going to test them with another solver I've been experimenting with.

[leonardoalt]

Btw by abstracting hard math functions (mul div mod) as nondeterministic values (a PR I'm working on) I get the SMTChecker to go through the original issue.

[leonardoalt]

So, I still don't think this is a bug, but rather out of resources. Should we remove the bug label/rename the issue? @bshastry @cameel

[cameel]

Yeah, I would not really call this a bug.