Spacer hitting unreachable code

[TaoBi22]

Running Z3 on current head hits unreachable code given the following input (reduced with ddSMT):

(set-logic HORN)
(declare-fun F ((_ BitVec 1) (_ BitVec 1) (_ BitVec 1) (_ BitVec 16) (_ BitVec 1) (_ BitVec 1) (_ BitVec 3) (_ BitVec 16) (_ BitVec 1) (_ BitVec 3) (_ BitVec 1)) Bool)
(declare-fun F_ ((_ BitVec 1) (_ BitVec 1) (_ BitVec 1) (_ BitVec 16) (_ BitVec 1) (_ BitVec 1) (_ BitVec 3) (_ BitVec 16) (_ BitVec 1) (_ BitVec 3) (_ BitVec 1)) Bool)
(assert (forall ((t (_ BitVec 16))) (F (_ bv0 1) (_ bv1 1) (_ bv1 1) (_ bv1 16) (_ bv1 1) (_ bv0 1) (_ bv0 3) t (_ bv0 1) (_ bv0 3) (_ bv0 1))))
(assert (or (F (_ bv0 1) (_ bv0 1) (_ bv0 1) (_ bv0 16) (_ bv0 1) (_ bv0 1) (_ bv0 3) (_ bv0 16) (_ bv0 1) (_ bv0 3) (_ bv0 1))))
(assert (forall ((t (_ BitVec 1)) (m (_ BitVec 1)) (tm (_ BitVec 1)) (p (_ BitVec 16)) (mp (_ BitVec 1)) (tmp (_ BitVec 1)) (_ (_ BitVec 3)) (p_ (_ BitVec 16)) (mp_ (_ BitVec 1)) (tmp_ (_ BitVec 3)) (_5 (_ BitVec 1))) (or (not (F t m tm p mp tmp _ p_ mp_ tmp_ _5)) (F_ (_ bv0 1) (_ bv0 1) (_ bv0 1) (_ bv0 16) (_ bv0 1) (_ bv0 1) (_ bv0 3) (bvadd p_ (_ bv1 16)) (_ bv0 1) (_ bv0 3) (_ bv0 1)))))
(check-sat)

Output is:

ASSERTION VIOLATION
File: ../src/util/hashtable.h
Line: 213
UNEXPECTED CODE WAS REACHED.
Z3 4.15.4.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new

Looks like it might be trying to build an overly ambitious table?

[NikolajBjorner]

It uses the hash-table here and runs out of resources (this should be dealt with by an exception).
To instead:
z3 7952.smt2 -v:2 fp.engine=spacer