NRA formula assertion violation

[wintered]

On the following formula z3 crashes with assertion violation (We configured z3 with the -d option).

(set-logic NRA)
(declare-fun a () Real)
(assert  
    (forall ((|| Real) )
        (exists ((b Real) )
            (forall ((c Real) )
                (exists ((d Real) )
                    (forall ((r Real) )
                        (exists ((e Real) )
                            (forall ((y Real) )
                                (exists ((f Real) )
                                    (let ((t (<= r 3)) (g 7)(h 7)(i 5)(j y)) 
                                    (let ((k (<= j i)) (l 0)) 
                                    (let ((u (<= b l)) (v (<= e h)) (m 0)(n  ||)) 
                                    (let ((o (<= n m)) (w (<=  c g)) (p f))                       
                                    (let ((q (<= (+ d p) 2))) (or  q  w o  v  u  k t)))))))))))))) 
)
(assert (exists ((s Real)) (forall ((x Real)) (or (and (>= a 0) (= x 0)) (= s 0))) ))
(check-sat)

ASSERTION VIOLATION
File: ../src/nlsat/nlsat_solver.cpp
Line: 1284
check_satisfied(m_clauses)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

OS: Ubuntu 18.04
Revision: 77ef40a

[NikolajBjorner]

duplicate of #2567