[SMTChecker] Error with CHC engine, non-zero timeout and an assert: `thread constructor failed: Resource temporarily unavailable`

[cameel]

When I try to run SMTChecker with a piece of code that contains assert(true) or assert(false), I get a weird error:

Unknown exception during compilation: thread constructor failed: Resource temporarily unavailable

It does not happen if I remove "engine": "chc" or "timeout" or use a timeout of zero. Seems to be a JS problem because the same input works fine with solc.

input.json

{
    "language": "Solidity",
    "settings": {
        "modelChecker": {
          "engine": "chc",
          "timeout": 20000
        }
    },
    "sources": {
        "C.sol": {
            "content": "contract C { function f() public { assert(true); } }"
        }
    }
}

solcjs output

Compiler version: 0.8.6

cat input.json | ./solcjs --standard-json

{
    "errors": [
        {
            "component": "general",
            "formattedMessage": "Unknown exception during compilation: thread constructor failed: Resource temporarily unavailable",
            "message": "Unknown exception during compilation: thread constructor failed: Resource temporarily unavailable",
            "severity": "error",
            "type": "Exception"
        }
    ],
    "sources": {
        "C.sol": {
            "id": 0
        }
    }
}

solc output

The problem does not happen with solc.

cat input.json | solc --standard-json

Compiler version: 0.8.6

{
    "errors": [
        {
            "component": "general",
            "errorCode": "1878",
            "formattedMessage": "Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing \"SPDX-License-Identifier: <SPDX-License>\" to each source file. Use \"SPDX-License-Identifier: UNLICENSED\" for non-open-source code. Please see https://spdx.org for more information.\n--> C.sol\n\n",
            "message": "SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing \"SPDX-License-Identifier: <SPDX-License>\" to each source file. Use \"SPDX-License-Identifier: UNLICENSED\" for non-open-source code. Please see https://spdx.org for more information.",
            "severity": "warning",
            "sourceLocation": {
                "end": -1,
                "file": "C.sol",
                "start": -1
            },
            "type": "Warning"
        },
        {
            "component": "general",
            "errorCode": "3420",
            "formattedMessage": "Warning: Source file does not specify required compiler version! Consider adding \"pragma solidity ^0.8.6;\"\n--> C.sol\n\n",
            "message": "Source file does not specify required compiler version! Consider adding \"pragma solidity ^0.8.6;\"",
            "severity": "warning",
            "sourceLocation": {
                "end": -1,
                "file": "C.sol",
                "start": -1
            },
            "type": "Warning"
        },
        {
            "component": "general",
            "errorCode": "2018",
            "formattedMessage": "Warning: Function state mutability can be restricted to pure\n --> C.sol:1:14:\n  |\n1 | contract C { function f() public { assert(true); } }\n  |              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n\n",
            "message": "Function state mutability can be restricted to pure",
            "severity": "warning",
            "sourceLocation": {
                "end": 50,
                "file": "C.sol",
                "start": 13
            },
            "type": "Warning"
        },
        {
            "component": "general",
            "errorCode": "6328",
            "formattedMessage": "Warning: CHC: Assertion violation might happen here.\n --> C.sol:1:36:\n  |\n1 | contract C { function f() public { assert(true); } }\n  |                                    ^^^^^^^^^^^^\n\n",
            "message": "CHC: Assertion violation might happen here.",
            "severity": "warning",
            "sourceLocation": {
                "end": 47,
                "file": "C.sol",
                "start": 35
            },
            "type": "Warning"
        }
    ],
    "sources": {
        "C.sol": {
            "id": 0
        }
    }
}

[cameel]

Pinging @leonardoalt.

[Bhanu-Partap]

Any solution for this issue. I am also facing the same error.