Hardhat compile w/ SMTChecker crashes with out-of-memory related issues on Ubuntu

I am using hardhat and trying to run the SMTChecker. Normal compilation (sans checker) works fine, but a very simple contract (e.g., just `AccessControl`), will consistently cause a crash, apparently due to running out of memory (the particular error message varies, but I have seen the crash occur at the point that total system memory usage maxes out). This should repro on Ubunto 20.04 and 22.04.1, and on solidity 0.8.9 , 0.8.15, and 0.8.16, and with or without high system memory usage prior to compilation. The issue doesn't repro with a completely empty contract, but will repro when an empty contract imports `AccessControl`. `AccessControl` is a pretty fundamental tool, so I think the checker is hard to use for much if it crashes on even that. In one case, I tried to use the `contracts` setting to limit the checker to just the main contract, but this didn't work for my complex contract. I also tried turning off optimization for the dummy contract, but this didn't seem to help.

Follow up question - since SMTChecker isn't working, what _should_ i do?
There are an enormous number of verification options, and I'm having a hard time figuring out which is best.
Ideally, I'd like something pretty rigorous (or else I might as well just test) but also pretty easy to use.
Since I've already written a bunch of assertions targeting the SMTChecker, ideally I'd get some other system to check these assertions, perhaps w/ minor tweaks.
Thanks!

Example error message:
```
Press ENTER or type command to continue
An unexpected error occurred:

RangeError [ERR_CHILD_PROCESS_STDIO_MAXBUFFER]: stdout maxBuffer length exceeded
at new NodeError (node:internal/errors:371:5)
at Socket.onChildStdout (node:child_process:461:14)
at Socket.emit (node:events:520:28)
at Socket.emit (node:domain:475:12)
at addChunk (node:internal/streams/readable:315:12)
at readableAddChunk (node:internal/streams/readable:285:11)
at Socket.Readable.push (node:internal/streams/readable:228:10)
at Pipe.onStreamRead (node:internal/stream_base_commons:190:23) {
code: 'ERR_CHILD_PROCESS_STDIO_MAXBUFFER',
cmd: '/home/un/.cache/hardhat-nodejs/compilers/linux-amd64/solc-linux-amd64-v0.8.9+commit.e5eed63a --standard-json'
}

shell returned 1
```

## Environment

- Compiler version: 0.8.9, 0.8.15, 0.8.16
- Target EVM version (as per compiler settings): IDK?
- Framework/IDE (e.g. Truffle or Remix): vim lol
- EVM execution environment / backend / blockchain client: IDK? just trying to compile w/ checks
- Operating system: Ubuntu 20.04, Ubuntu 22.04.1

## Steps to Reproduce

Contract:
```
// Contract based on https://docs.openzeppelin.com/contracts/3.x/erc1155
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.9;

import "@openzeppelin/contracts/access/AccessControl.sol";

contract Ctr is AccessControl {
}
```

Hardhat config:
```
/**
* @type import('hardhat/config').HardhatUserConfig
*/
module.exports = {
solidity: {
version: "0.8.9",
settings: {
optimizer: {
enabled: true,
runs: 1000
},
modelChecker: {
engine: 'all',
}
}
},
networks: {
hardhat: {},
},
}
```
run `npx hardhat compile`

Reproduce with the shown AccessControl contract, Hardhat config, and `npx hardhat compile` using the listed Solidity versions on Ubuntu. Start at the SMTChecker compilation path and its child-process output handling, then verify that compiling this import no longer exhausts memory or hits the stdout maxBuffer error while checker diagnostics remain usable.

Written by the indexing model from the issue text.