`Z3_set_param_value(cfg, "timeout", "10")` 中的未知参数 `timeout`；

Question

设置超时一直是一个热门话题，相关的回答也很多，但是Z3(4.4.2)最新的unstable-branch出现了一个新的警告(Ubuntu-12.04-64 ).

纯C API在我的项目中使用，我使用Z3_assert_cnstr()添加约束，Z3_check_and_get_model()检查结果。

我将超时设置为：

Z3_set_param_value(cfg, "timeout", "10");

10 毫秒。

当我运行这个项目的时候，有这样的警告：

WARNING: unknown parameter 'timeout'
Legal parameters are:
auto_config (bool) (default: true)
debug_ref_count (bool) (default: false)
dump_models (bool) (default: false)
model (bool) (default: true)
model_validate (bool) (default: false)
proof (bool) (default: false)
rlimit (unsigned int) (default: 4294967295)
smtlib2_compliant (bool) (default: false)
timeout (unsigned int) (default: 4294967295)
trace (bool) (default: false)
trace_file_name (string) (default: z3.log)
type_check (bool) (default: true)
unsat_core (bool) (default: false)
well_sorted_check (bool) (default: false)

并且从规范来看，"timeout"是一个合法的参数。

有什么我遗漏的吗？

我测试使用“10u”而不是“10”作为第三个参数来指示无符号数，但是，没有任何改变。此外，从 master 分支修复的 ASSERTION VIOLATION 是我使用 unstable-branch 的原因。

Answer 1

查看HERE源代码，我认为

中存在错误

void set    (   char const *    param,
                char const *    value 
            )

下面的if

if (p == "rlimit")

应该是

else if (p == "rlimit")

避免错误的错误。

查看 HERE GitHub 的当前提交，已于 10 月 7 日更正。

`Z3_set_param_value(cfg, "timeout", "10")` 中的未知参数 `timeout`；

Unknown parameter `timeout` in `Z3_set_param_value(cfg, "timeout", "10")`;

c

api

z3