z3 process continues to run after CBMC process is terminated

[zhassan-aws]

CBMC version: 6.3.1
Operating system: Ubuntu 20.04
Exact command line resulting in the issue: cbmc hard.c --z3

When I run CBMC and then kill the process using kill -9, the z3 process continues to run.

Here's an example session:

$ pgrep z3
$ cat hard.c 
# include <assert.h>

int main() {
    const int SZ = 10000;
    int a[SZ];

    int x;
    int i;

    for (i = 0; i < SZ; i++) {
        a[i] = x;
    }

    unsigned j;
    assert(j >= SZ || a[j] == x);
    
    return 0;
}
$ cbmc hard.c --z3 >& /dev/null &
[1] 3438130
$ sleep 5
$ kill -9 3438130
$ 
[1]+  Killed                  cbmc hard.c --z3 &> /dev/null
$ sleep 5
$ pgrep z3
3438155
$ sleep 5
$ pgrep z3
3438155

[hanno-becker]

I experience the same issue.

[rod-chapman]

Same with Bitwuzla. Killing the CBMC process with Ctrl-C does not stop the underlying prover which continues to run and consume memory and (lots of) CPU time.