#z3/build-2020-02-17-41ab578/z3 bug.smt2
ASSERTION VIOLATION
File: ../src/ast/macros/macro_util.cpp
Line: 440
is_macro_head(head, head->get_num_args())
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
^C^C
#cat bug.smt2                           
(declare-fun f ((_ BitVec 1)) Bool)
(declare-fun g ((_ BitVec 1)) (_ BitVec 1))
(assert (forall ((x (_ BitVec 1))) (f (g x))))
(check-sat-using bv)