Assertion violation for quantified LIRA in new core

[joe-hauns]

z3 runs into "unexpected code" when running with the new core on the following problem:

(set-logic ALL)

(assert (not 
  (forall ((x Real) (d Real)) 
      (exists ((y Real))
        (= (+ (* 3 x) d) (+ y (to_int y) (to_int (- y))) )
      )
  )
))

(check-sat)
(get-model)

Output:

############################################
running z3 -T:1 sat.euf=true sat.smt=true problem.smt2
............................................

Asserting this expression twice in a row:
 (not p!6)
ASSERTION VIOLATION
File: ../src/qe/qsat.cpp
Line: 581
UNEXPECTED CODE WAS REACHED.
Z3 4.12.3.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new