$ z3 model_validate=true bug.smt2
constraint 32 violated
number of constraints = 44
(0) j0 >= 1
(1) j0 <= 1
(2) j1 >= 1
(3) j1 <= 1
(4) j2 >= 0
(5) j2 <= 0
(6) j3 >= 0
(7) j3 <= 0
(8)  - j4 + j5 <= 0
(10)  - j4 + j5 >= 0
(12) j9 >= 1/11
(13) j9 <= 1/11
(14) j14 - j15 <= 0
(15) j14 - j15 >= 0
(16)  - j18 + j19 <= 0
(18)  - j18 + j19 >= 0
(20) j1 + j15 <= 0
(22) j1 + j15 >= 0
(28)  - j7 - j10 + j15 <= 0
(31)  - j15 + j10 + j7 < 1
(32) j10 - j27 <= 1
(34) j10 - j27 >= 1
(36)  - j19 + j5 <= 0
(38)  - j19 + j5 >= 0
(41) j8 + j9 - j10 + j11 - 1/11*j5 > 0
(42) j8 + j9 - j10 + j11 - 1/11*j5 >= 0
ASSERTION VIOLATION
File: ../src/math/lp/nra_solver.cpp
Line: 234
UNEXPECTED CODE WAS REACHED.
Z3 4.15.5.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
$ cat bug.smt2
(declare-fun v0 () Real) 
(declare-fun v1 () Real) 
(assert (= (+ 1 0 (* (- (* (/ 1 0) (+ (- (/ 1 11)) v0 v1)) (+ (- (/ 1 11)) v0)) 
(- (* (/ 1 (div (+ 1 v0 v1) 1)) (+ (- (/ 1 11)) v0 v1)) (+ (- (/ 1 11)) v0)))) v0)) 
(check-sat)       
``