时间戳

首页 > 解决方案 > z3.parse_smt2_string 在 int2bv 上失败

python - z3.parse_smt2_string 在 int2bv 上失败

问题描述

当我使用parse_smt2_string文档中的示例字符串时，它可以正常工作。但是，在 int2bv 上解析失败。我该如何诊断？

>>> 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'

标签： pythonpython-3.xz3z3py

解决方案

这与 无关int2bv，而是因为您没有在顶层提供有效的 SMTLib 行。例如，以下是有效的：

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

在顶层，您可以拥有声明、断言或通用 SMTLib 命令，而不是独立的表达式。

推荐阅读