Soundness issue with `sat.cut=true sat.cut.aig=true`

z3 4.15.4 incorrectly reports unsat with `sat.cut=true sat.cut.aig=true` on the attached test case:

```
> z3 sat.cut=true sat.cut.aig=true redc.smt2
unsat
```

```
> z3 redc.smt2
sat
```

```
> bitwuzla redc.smt2
sat
```

[redc.smt2.gz](https://github.com/user-attachments/files/24091132/redc.smt2.gz)