Wrong verdict with (set-option :sat.smt true) #7990
Description
On the following file dglm.txt, Z3 returns a wrong verdict when configured with (set-option :sat.smt true). More precisely, it returns the wrong result on the very final call to (check-sat).
Result: SAT, after ~18secs on my machine.
Expected: UNSAT. Confirmed by Z3 with (set-option :sat.smt false) in around 30secs. Other SMT solvers also confirm this result.
Interestingly, when adding (set-option :model_validate true), Z3 reports (error "line ... column 10: an invalid model was generated") also for several intermediate (check-sat) calls, even though the SAT verdict is correct for those.
It seems the incremental inprocessing unsoundly deletes some irredundant clauses or fails to reconstruct them correctly.
Background: The task was generated by Dartagnan in the context of verifying a concurrent data structure.