Assertion failure in nlsat: m_cache.mk_unique(p) == p

[addisoncrump]

I am not quite sure how to diagnose this bug myself. It doesn't seem to me that this input is too complicated (though I wasn't expecting z3 to be able to solve it):

(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(assert (< 0 x))        
(assert (< x y))
(assert (< y z))
(assert (not (= y (* 2 x))))
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun e () Int)
(declare-fun f () Int)
(declare-fun g () Int)
(declare-fun h () Int)
(declare-fun i () Int)
(assert (< 0 h))
(assert (< h a))
(assert (< a f))
(assert (< f c))
(assert (< c e))
(assert (< e g))
(assert (< g d))
(assert (< d i))
(assert (< i b))
(assert (= y (* (- e a) (+ e a))))
(assert (= y (* (- i e) (+ i e))))
(assert (= x (* (- e c) (+ e c))))
(assert (= x (* (- g e) (+ g e))))
(assert (= (- x y) (* (- e d) (+ e d))))
(assert (= (- x y) (* (- f e) (+ f e))))
(assert (= (+ x y) (* (- e h) (+ e h))))
(assert (= (+ x y) (* (- b e) (+ b e))))
(check-sat)
ASSERTION VIOLATION
File: /builddir/build/BUILD/z3-z3-4.12.2/src/nlsat/nlsat_solver.cpp
Line: 2511
Failed to verify: m_cache.mk_unique(p) == p

4.12.2.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new

I would diagnose myself and help find a root cause, but I'm really not sure where to start :sweat_smile: