Soundness bug/Invalid model on simple formula #4100
Description
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