Call bitwuzla with a max amount of memory to use

[gustavo-grieco]

For large or complex code, hevm produces some SMT formulas that will cause bitwuzla to consume large amounts of memory (and crash or be killed by the OS). To avoid that, bitwuzla has a parameter to control the maximum amount of memory used:

-M <n>, --memory-limit <n>        set maximum memory limit in MB per satisfiability check 

Please consider controlling this parameter from hevm that sets the max memory to the physical memory available divided by the number of solvers.

[msooseth]

Honestly, the best would be to have a separate runner that actually kills the process if it runs too long/take too much mem. More reliable than telling the SMT solver to restrict itself. Many systems have trouble properly assessing and restricting their memory usage. Very much related is to what @karmacoma is doing here: https://github.com/a16z/jsi Unfortunately that doesn't (yet) support interactive SMT calls, but maybe it's not impossible to add. Also a lot of ❤ to @0xkarmacoma that piece of software is amazing. It could become something that many people use for their daily use-case.

Related Twitter thread (I hate twitter): https://x.com/0xkarmacoma/status/1915903241868742741