z3.parse_smt2_string fails on int2bv

When I use parse_smt2_string on the example string from the docs, it works correctly. However, the parsing fails on int2bv. How can I diagnose this?

>>> import z3
>>> z3.parse_smt2_string('(declare-const x Int) (assert (> x 0)) (assert (< x 10))')
[x > 0, x < 10]
>>> z3.parse_smt2_string('((_ int2bv 1) 1)')
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "/home/elliot/miniconda3/envs/angr/lib/python3.6/site-packages/z3_solver-4.8.7.0-py3.6-linux-x86_64.egg/z3/z3.py", line 8601, in parse_smt2_string
    return AstVector(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
  File "/home/elliot/miniconda3/envs/angr/lib/python3.6/site-packages/z3_solver-4.8.7.0-py3.6-linux-x86_64.egg/z3/z3core.py", line 3222, in Z3_parse_smtlib2_string
    _elems.Check(a0)
  File "/home/elliot/miniconda3/envs/angr/lib/python3.6/site-packages/z3_solver-4.8.7.0-py3.6-linux-x86_64.egg/z3/z3core.py", line 1381, in Check
    raise self.Exception(self.get_error_message(ctx, err))
z3.z3types.Z3Exception: b'(error "line 1 column 2: invalid command, symbol expected")\n'

Solution

This has nothing to do with int2bv, but rather due to the fact that you've not provided a line that is valid SMTLib at the top-level. The following, for instance, works:

>>> z3.parse_smt2_string('(assert (= #b1 ((_ int2bv 1) 1)))')
[1 == int2bv(1)]

At the top-level, you can have declarations, assertions, or general SMTLib commands, not a standalone expression.