[soundness] QF_UFIDL: sat on Z3-unsat vhard7.smt2 (SMT-LIB) #50

Summary

Differential vs Z3 4.16.0: OxiZ returns sat on vhard7 where Z3 returns unsat.

Unsound sample

Repro

f=non-incremental/QF_UFIDL/mathsat/EufLaArithmetic/vhard/vhard7.smt2
z3 "$f"       # unsat
oxiz -q "$f"  # sat (observed on upstream and integrate)

Notes

EUF + difference-logic / LIA arithmetic hard case from mathsat suite.