FPA soundness issue in incremental solving still exists

[ThomasMayerl]

Unfortunately, PR #8712 did not solve issue #8345 (I cannot reopen the issue) for the examples posted in the issue.

For example, the solver still incorrectly reports unsat in the following example. Removing the push changes the output to sat:

(declare-fun int_to_fp (Int) (_ FloatingPoint 5 11))

; Definition of int_to_fp as composition of int2bv and to_fp
(assert (forall ((i Int))
(!  (= (int_to_fp i) ((_ to_fp 5 11) ((_ int2bv 16) i)))
    :pattern ((int_to_fp i))
    :qid |int_to_fp_def|
)))

; Should trivially follow from the axiom above, but for some reason required for the issue
(assert (forall ((i Int) (j Int))
    (! (and (= (fp.to_real (fp.add RNE (int_to_fp i) (int_to_fp j))) (fp.to_real (fp.add RNE ((_ to_fp 5 11) ((_ int2bv 16) i)) ((_ to_fp 5 11) ((_ int2bv 16) j)))))
            (= (fp.to_real (fp.sub RNE (int_to_fp i) (int_to_fp j))) (fp.to_real (fp.sub RNE ((_ to_fp 5 11) ((_ int2bv 16) i)) ((_ to_fp 5 11) ((_ int2bv 16) j)))))
        )
    :pattern ((int_to_fp i) (int_to_fp j))
    :qid |int_to_fp_ax|
    )
))

(push)
(declare-fun triggering_term ((_ FloatingPoint 5 11)) (Bool))

(assert (triggering_term (int_to_fp 16384))) ; 2.0
(assert (triggering_term (int_to_fp 15820))) ; ~0.1
(check-sat)