[543] % z3 small.smt2
ASSERTION VIOLATION
File: ../src/ast/rewriter/rewriter_def.h
Line: 50
v->get_sort() == m().get_sort(r)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[544] % 
[544] % cat small.smt2
(set-option :smt.quasi_macros true)
(declare-sort a)
(declare-sort b)
(declare-sort c)
(declare-fun d (c a) b)
(declare-fun k () c)
(declare-fun i () c)
(declare-fun e (b) a)
(declare-fun f (b) a)
(declare-fun j (b b) Bool)
(assert (forall ((g a)) (let ((h (d i g))) (j (d i (f (d k (e h)))) h))))
(check-sat)
[545] %