% z3 bug.smt2
ASSERTION VIOLATION
File: ../src/smt/smt_internalizer.cpp
Line: 475
b_internalized(n)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
ASSERTION VIOLATION
File: ../src/util/old_vector.h
Line: 375
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
% cat bug.smt2
(set-option :trace  true)  
(declare-fun a () Real) 
(declare-fun b () Real)  
(declare-fun c () Real) 
(declare-fun d () Real) 
(declare-fun g () Real) 
(declare-fun e () Real) 
(declare-fun f () Real) 
(assert (not (= 0 d))) 
(assert (not (= (and (= c f)(< (* (+ (* (mod b g) e))) 0.0 e a)  
(<= 0.0 b g))(< 0 (*(+ e (mod b f))) 0))))  
(check-sat)