qffd smt parallel Invalid model on QF_LRA formula

[muchang]

Hi,
For this formula:

(set-option :model_validate true)
(declare-fun a () Real)
(assert (= a 1))
(check-sat-using (then qffd smt))

Z3 parallel.enable=true gives an invalid model:

[568] % z3 small.smt2
sat
[569] % z3 parallel.enable=true small.smt2
failed to verify: (= a 1.0)
evaluated to false
(params override_incremental true keep_cardinality_constraints true pb.solver solver xor_solver false inprocess.max 2 restart.max 5000 lookahead_simplify true retain_blocked_clauses false max_conflicts 4294967295)
(= a 1.0) |-> 0
sat
(error "line 4 column 32: an invalid model was generated")
[570] % 
[570] % cat small.smt2
(set-option :model_validate true)
(declare-fun a () Real)
(assert (= a 1))
(check-sat-using (then qffd smt))
[571] %

OS: Ubuntu 18.04
Commit: f447292

[rainoftime]

@muchang, Acccording to #3640

then don't use qffd on something that isnt fd

It seems that when using qffd or psat for real/int formulas, the model validator can often report Invalid model

[rainoftime]

Possibly related case 1: (from #3737)

(set-logic QF_FD)
(set-option :model_validate true)
(set-option :parallel.enable true)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const i3 Int)
(declare-const i4 Int)
(declare-const v7 Bool)
(declare-const i5 Int)
(declare-const i6 Int)
(declare-const v8 Bool)
(declare-const v10 Bool)
(assert (or (> 56 i3) v2 v1 v5 v3 v1 v8))
(assert (or (< 56 (- i4)) v5 (< i3 56)))
(assert (or (=> v1 (=> v2 v7)) v0 v5))
(assert v10)
(assert (= i5 i6))
(assert v8)
(assert (or v7 v1 v3))
(assert (or (< 56 (- i4)) v2 v5))
(assert v6)
(assert (or v3 (< 56 (- i4)) v1))
(assert (or v0 v0 (and v2 v5 v2)))
(check-sat)

[rainoftime]

Possibly related test case 2 (from #3736)

(set-logic LRA)
(declare-fun _substvar_87_ () Bool)
(set-option :model_validate true)
(set-option :parallel.enable true)
(declare-const r10 Real)
(assert (exists ((q1 Bool) (q2 Real) (q3 Bool)) (> r10 6.0)))
(assert _substvar_87_)
(check-sat-using (then add-bounds unit-subsume-simplify qffd))