Z3py：parse_smt2_file 引发异常

Question

我正在尝试在我的 python 文件

ctx = Context()
s = Solver(ctx=ctx)
f = parse_smt2_file("./Encodings/foo.smt2", ctx=ctx)
s.add(f)

我遇到了以下问题：

Traceback (most recent call last): File "", line 1, in f = z3.parse_smt2_file("./ex.smt2", ctx=ctx) File "X/Applications/z3-4.3.3.376614a7822d-x64-osx-10.9.5/bin/z3.py", line 7305, in parse_smt2_file return _to_expr_ref(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx) File "X/Applications/z3-4.3.3.376614a7822d-x64-osx-10.9.5/bin/z3core.py", line 2947, in Z3_parse_smtlib2_file raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err)) Z3Exception: parser error

知道问题出在哪里吗？

Answer 1

问题是文件由

完成

(check-sat)
(get-model)

我删除了这行并且有效

Z3py：parse_smt2_file 引发异常

Z3py: parse_smt2_file raises Exception

z3

z3py