c语言 - "Z3_set_param_value(cfg， "timeout"， "10" )"中的未知参数"超时";

Question

设置超时一直是一个热门话题，有很多相关的答案，但在Z3（4.4.2）（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)

从规范来看，"超时"是一个合法参数。

我错过了什么吗？

我测试使用"10u"而不是"10"作为第三个参数来表示无符号数字，但没有任何变化。此外，从master分支修复的ASSERTION VIOLATION是我使用不稳定分支的原因。

Answer 1

查看源代码，我认为中有一个错误

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

下方的if

if (p == "rlimit") 

应该是

else if (p == "rlimit")

以避免出现错误。

看看GitHub上的当前提交，它在10月7日被更正。