If an SMT solver starts eating memory like an ever-hungry cookie monster, it should be killed. This is quite easy to achieve at least on Unix, via ulimit -m. The kernel will kill the process. This can be important, as a single badly behaving SMT solver could otherwise eat all the memory and make the other solvers crash due to OOM.