Assertion violation at ../src/smt/theory_bv.cpp: 298

[merlinsun]

Hi,
For this instance, z3 d5d77df

$ z3 small.smt2
ASSERTION VIOLATION
File: ../src/smt/theory_bv.cpp
Line: 298
th_id == null_theory_id
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
s
Segmentation fault (core dumped)
$ cat small.smt2
(assert (forall ((e (_ FloatingPoint 2 3))) (distinct (_ bv0 1) (ite (fp.lt (_ +zero 2 6) (fp (_ bv0 1) (_ bv0 2) (_ bv0 5))) (_ bv1 1) (_ bv0 1)))))
(check-sat-using (then bit-blast unit-subsume-simplify))