@override Z3_ast build(Context c) { final a = c._createAST(arg); return c._z3.mk_extract(high, low, a); }