Soundness issue with sat.cut=true sat.cut.aig=true #8063
Description
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