(set-option :smt.threads 4)   
(declare-fun c () ( Array Int Int )) 
(declare-fun a () ( Array Int Int )) 
(declare-fun arr () ( Array Int Int ))
(declare-fun d () Int) 
(declare-fun u () Int) 
(declare-fun i () Int) 
(assert (let (( ?g (select arr i)) (?e (select a 0)) (d d)) 
(and (forall (( ?j Int )) (xor (and (= d u)) 
     (forall (( ?f Int )) (<= (select arr ?f) (select arr ?j)))))( <= ?e ?g ) 
     (forall (( ?h Int )) (= (and (<=  d ?h 0))(= (select arr ?h ) 0)))(= (select c d) d)))) 
(check-sat)

ASSERTION VIOLATION
File: ../src/ast/rewriter/rewriter_def.h
Line: 589
frame_stack().empty()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB