Invalid model for incremental QF_LRA instance (rewriter.hoist_cmul)

[rainoftime]

Hi, for the following formula (which has two (check-sat) commands),

(set-logic QF_LRA)
(set-option :model_validate true)
(set-option :rewriter.hoist_cmul true)
(declare-const v0 Bool)
(declare-const r0 Real)
(declare-const r1 Real)
(assert (=> (<= r0 (- r1 r0 r0 r0) r0) (<= r0 (- r1 r0 r0 r0) r0)))
(declare-const v1 Bool)
(declare-const v2 Bool)
(assert (or (=> (<= r0 (- r1 r0 r0 r0) r0) (<= r0 (- r1 r0 r0 r0) r0)) (<= r0 (- r1 r0 r0 r0) r0)))
(assert (or (=> (<= r0 (- r1 r0 r0 r0) r0) (<= r0 (- r1 r0 r0 r0) r0)) v2 (xor (<= r0 (- r1 r0 r0 r0) r0) (<= r0 (- r1 r0 r0 r0) r0) v1 v0 v1 (<= r0 (- r1 r0 r0 r0) r0) (<= r0 (- r1 r0 r0 r0) r0) v1) v1 (xor (<= r0 (- r1 r0 r0 r0) r0) (<= r0 (- r1 r0 r0 r0) r0) v1 v0 v1 (<= r0 (- r1 r0 r0 r0) r0) (<= r0 (- r1 r0 r0 r0) r0) v1) (xor (<= r0 (- r1 r0 r0 r0) r0) (<= r0 (- r1 r0 r0 r0) r0) v1 v0 v1 (<= r0 (- r1 r0 r0 r0) r0) (<= r0 (- r1 r0 r0 r0) r0) v1) (distinct r1 r0) (<= r0 (- r1 r0 r0 r0) r0) (distinct r1 r0) (xor (<= r0 (- r1 r0 r0 r0) r0) (<= r0 (- r1 r0 r0 r0) r0) v1 v0 v1 (<= r0 (- r1 r0 r0 r0) r0) (<= r0 (- r1 r0 r0 r0) r0) v1) v1))
(push 1)
(declare-const r2 Real)
(assert (distinct r1 r0))
(assert (and (xor (<= r0 (- r1 r0 r0 r0) r0) (<= r0 (- r1 r0 r0 r0) r0) v1 v0 v1 (<= r0 (- r1 r0 r0 r0) r0) (<= r0 (- r1 r0 r0 r0) r0) v1) v1 (> r1 (- (- r1 r0 r0 r0)) r2 (- r1 r0 r0 r0)) (or (=> (<= r0 (- r1 r0 r0 r0) r0) (<= r0 (- r1 r0 r0 r0) r0)) v2 (xor (<= r0 (- r1 r0 r0 r0) r0) (<= r0 (- r1 r0 r0 r0) r0) v1 v0 v1 (<= r0 (- r1 r0 r0 r0) r0) (<= r0 (- r1 r0 r0 r0) r0) v1) v1 (xor (<= r0 (- r1 r0 r0 r0) r0) (<= r0 (- r1 r0 r0 r0) r0) v1 v0 v1 (<= r0 (- r1 r0 r0 r0) r0) (<= r0 (- r1 r0 r0 r0) r0) v1) (xor (<= r0 (- r1 r0 r0 r0) r0) (<= r0 (- r1 r0 r0 r0) r0) v1 v0 v1 (<= r0 (- r1 r0 r0 r0) r0) (<= r0 (- r1 r0 r0 r0) r0) v1) (distinct r1 r0) (<= r0 (- r1 r0 r0 r0) r0) (distinct r1 r0) (xor (<= r0 (- r1 r0 r0 r0) r0) (<= r0 (- r1 r0 r0 r0) r0) v1 v0 v1 (<= r0 (- r1 r0 r0 r0) r0) (<= r0 (- r1 r0 r0 r0) r0) v1) v1) v1 (or (=> (<= r0 (- r1 r0 r0 r0) r0) (<= r0 (- r1 r0 r0 r0) r0)) (<= r0 (- r1 r0 r0 r0) r0)) (distinct r1 r0) (=> (<= r0 (- r1 r0 r0 r0) r0) (<= r0 (- r1 r0 r0 r0) r0))))
(check-sat)
(push 1)
(declare-const v3 Bool)
(assert (= v0 (> r2 (- r1 r0 r0 r0) 88173.57679) (xor (<= r0 (- r1 r0 r0 r0) r0) (or (=> (<= r0 (- r1 r0 r0 r0) r0) (<= r0 (- r1 r0 r0 r0) r0)) (<= r0 (- r1 r0 r0 r0) r0)) v2 (>= (- r1 r0 r0 r0) (- (- r1 r0 r0 r0))) (> r1 (- (- r1 r0 r0 r0)) r2 (- r1 r0 r0 r0)) v1 (> r1 (- (- r1 r0 r0 r0)) r2 (- r1 r0 r0 r0)) v2 (xor (<= r0 (- r1 r0 r0 r0) r0) (<= r0 (- r1 r0 r0 r0) r0) v1 v0 v1 (<= r0 (- r1 r0 r0 r0) r0) (<= r0 (- r1 r0 r0 r0) r0) v1)) (> r1 (- (- r1 r0 r0 r0)) r2 (- r1 r0 r0 r0)) (distinct r1 r0) (distinct r1 r0)))
(declare-const v4 Bool)
(pop 1)
(check-sat)

When executing the command z3 fname.smt2 timeout=10000,
z3 (commit ae5a713) returns unknown for the first query, but gives an invaide model for the second query.

unknown
sat
(error "line 23 column 10: an invalid model was generated")

[rainoftime]

After removing (set-option :rewriter.hoist_cmul true), both queries can be answered correctly and fast.

[NikolajBjorner]

See #3836