Issue with tactic qsat

[merlinsun]

Hi,
For this following instance, z3 8061765 incorrectly gives unsat with (check-sat-using qsat).
It is unclear if this is related to #7217.

$ cat small.smt2 
(declare-const x Real)
(declare-fun s () Real)
(declare-fun o () Real)
(assert (and (or (> 1 1) (< x (* s s (- x 1.0))) (= 1.0 (/ s (* s (- 1))))) (or true (and (= 1.0 (/ 0 s)) (or (= o 0) (= s 1.0)) (= 1.0 1.0) (< o (* s x))))))
(check-sat-using qsat)
(check-sat)
$ z3 small.smt2 
unsat
sat

[NikolajBjorner]

C:\z3\build>z3 7376.smt2 smt.arith.validate=true
ASSERTION VIOLATION
File: C:\z3\src\smt\theory_lra.cpp
Line: 3461
Failed to verify: !m_core.empty() || !m_eqs.empty()

[levnach]

same issue as #7368