Support mixing low-level and high-level SMT APIs

[rbtying]

Since not all of the functions are supported in the high-level API (e.g. bvsgt for bitvectors), would it be possible to allow exposing those by having the low-level AST be usable mixed with the high-level API?