Issues with bvsmul_noovfl

[rainoftime]

Hi, for the following formula

(set-option :model_validate true)
(declare-fun bv_4-0 () (_ BitVec 1))
(assert (not (bvsmul_noovfl bv_4-0 bv_4-0)))
(check-sat)

z3 461e710 yields an invalid model

z3 delta.out.smt2 
sat
(error "line 4 column 10: an invalid model was generated")

[rainoftime]

(set-option :rewriter.flat false)
(declare-fun bv_18-0 () (_ BitVec 9))
(assert (exists ((q64 (_ BitVec 9))) (bvsmul_noovfl q64 bv_18-0)))
(check-sat-using qe_rec)

ASSERTION VIOLATION
File: ../src/qe/qsat.cpp
Line: 651
validate_defs("check_sat")
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[NikolajBjorner]

First one is taken care of. qe_rec and bvsmul is too exotic to merit time to debug. There are more important bugs.