Soundness bug/Invalid model on simple formula

[wintered]

Bizarrely the bug disappears when the unsat_core option is disabled. By replacing the (check-sat-using (then sat bv)) by (check-sat), I get unsat.

$z3release bug.smt2
sat
(error "line 4 column 30: an invalid model was generated")
$cat bug.smt2
(set-option :unsat_core true) 
(set-option :model_validate true) 
(assert (! (not (<= 0 0)) :named a)) 
(check-sat-using (then sat bv)) 

OS: Ubuntu 18.04
Commit: 785c9a1