(declare-fun a () Int)                                                          
(declare-fun b (Int Int) Int)                                                   
(declare-fun c (Int Int) Int)                                                   
(assert (forall ((d Int) (y Int))                                               
(= (c d y) (div d y) )))                                                        
(push) (assert (= (c (b 3 (b 3 a)) 3) 0))                                       
(check-sat)                                                                     
(pop)                                                                           
(check-sat)                                                                     
(assert (= (c (b 3 (b 3 a)) 3) 0))                                              
(check-sat) 

sat
sat
ASSERTION VIOLATION
File: ../src/smt/smt_internalizer.cpp
Line: 580
!e_internalized(n)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
ASSERTION VIOLATION
File: ../src/util/old_vector.h
Line: 370
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB