Invalid model on QF_FP formula

[wintered]

[762] % z3 parallel.enable=true model_validate=true small.smt2
sat
[763] % z3release model_validate=true small.smt2
sat
[764] % z3release parallel.enable=true model_validate=true small.smt2
sat
(error "line 7 column 10: an invalid model was generated")
[765] % 
[765] % cat small.smt2
(declare-fun a () Float16)
(declare-fun b () Float16)
(declare-fun c () Float16)
(declare-fun d () Float16)
(assert (= c (fp.rem a b)))
(assert (not (= c d)))
(check-sat)
[766] %

OS: Ubuntu 18.04
Commit: ee9c797

[levnach]

Valgrind finds a problem:
valgrind ./z3 ~/Dropbox/smts/3897.smt2 parallel.enable=true model_validate=true
==20420== Memcheck, a memory error detector
==20420== Copyright (C) 2002-2017, and GNU GPL'd, by Julian Seward et al.
==20420== Using Valgrind-3.13.0 and LibVEX; rerun with -h for copyright info
==20420== Command: ./z3 /home/lev/Dropbox/smts/3897.smt2 parallel.enable=true model_validate=true
==20420==
==20420== Conditional jump or move depends on uninitialised value(s)
==20420== at 0x7F2CD9: sat::solver::copy(sat::solver const&, bool) (sat_solver.cpp:222)
==20420== by 0x16DD84A: inc_sat_solver::translate(ast_manager&, params_ref const&) (inc_sat_solver.cpp:123)
==20420== by 0xAE08BB: parallel_tactic::operator()(ref const&, sref_buffer<goal, 16u>&) (parallel_tactic.cpp:720)
==20420== by 0x6C55FC: cond_tactical::operator()(ref const&, sref_buffer<goal, 16u>&) (tactical.cpp:1031)
==20420== by 0x6C55D3: cond_tactical::operator()(ref const&, sref_buffer<goal, 16u>&) (tactical.cpp:1029)
==20420== by 0x6C046E: and_then_tactical::operator()(ref const&, sref_buffer<goal, 16u>&) (tactical.cpp:120)
==20420== by 0x6C046E: and_then_tactical::operator()(ref const&, sref_buffer<goal, 16u>&) (tactical.cpp:120)
==20420== by 0x6C046E: and_then_tactical::operator()(ref const&, sref_buffer<goal, 16u>&) (tactical.cpp:120)
==20420== by 0x6C55D3: cond_tactical::operator()(ref const&, sref_buffer<goal, 16u>&) (tactical.cpp:1029)
==20420== by 0x6C55FC: cond_tactical::operator()(ref const&, sref_buffer<goal, 16u>&) (tactical.cpp:1031)
==20420== by 0x6C55FC: cond_tactical::operator()(ref const&, sref_buffer<goal, 16u>&) (tactical.cpp:1031)
==20420== by 0x6C55FC: cond_tactical::operator()(ref const&, sref_buffer<goal, 16u>&) (tactical.cpp:1031)

[NikolajBjorner]

We have to treat it as a duplicate of #2381 where the repro is more straight-forward.
Model validation succeeds between the bit-blasted formulas and the SAT solver, so the discrepancy is above (in the bit-blasting vs. rewriting semantics of fp.rem).