(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun o () Int)
(declare-fun e () Int)
(declare-fun f () Int)
(declare-fun g (Int Int Int) Int)
(declare-fun h () Int)
(declare-fun i (Int) Int)
(declare-fun j (Int) Int)
(declare-fun k (Int) Int)
(declare-fun l (Int) Int)
(declare-fun m (Int) Bool)
(declare-fun n (Int) Bool)
(assert
(let ((p (n (i (i 0)))))
(let ((aa p) (ab (m 0)))
(let ((af (n 0)) (ag (or (m f) (n e))))
(let ((al (distinct 0 d)) (q (not (n (i 0)))) (an h) (aq (n 0)))
(let ((bs (ite ag (+ 1 c) c)))
(let ((av (ite af 0 bs)))
(let ((au (ite (not (distinct c av)) (+ 1 c) c)))
(let ((az b))
(let ((be (ite ab (- 0 8 av) av)))
(let ((bg (ite (and p (distinct au be)) (- au) au)))
(let ((bk (distinct b (k 0))))
(let ((cb (or (and (or (m (i 0)) p) (or  bk (= bg c))))))
(let ((ce (and ab (distinct (l 0) d))))
(let ((cq (g (ite (= an bs) 0 (ite (and ag (distinct c an)) 0 o)) 0 a)))
 (not
  (and al (= (ite ce av (ite af bs c)) au)
   (= (ite (not (distinct bg (ite aa (* 20 be) be)))
       (ite cb (g 0 (ite (or ab (and af bk)) a
                     (ite (and ab ag) (ite ag (g 0 a a) a) (ite q cq 0)))
                (ite (and ab (not (= b (j 0)))) a 0))
        (ite q cq (ite (or aq (and ag (= bg c)))
                   (g 0 a a) a))) 0) 0))))))))))))))))))
(check-sat)

ASSERTION VIOLATION
File: ../src/math/lp/int_solver.cpp
Line: 523
l <= new_val && new_val <= u
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB