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

【问题标题】：Unknown parameter `timeout` in `Z3_set_param_value(cfg, "timeout", "10")`;`Z3_set_param_value(cfg, "timeout", "10")` 中的未知参数`timeout`；
【发布时间】：2015-11-10 07:08:41
【问题描述】：

设置超时一直是一个热门话题，相关的答案也很多，但是在最新的Z3（4.4.2）（Ubuntu-12.04-64）的unstable-branch中出现了一个新的警告。

我的项目使用纯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”作为第三个参数来表示一个无符号数，但是没有任何改变。此外，从主分支修复的断言违规是我使用不稳定分支的原因。

【问题讨论】：

标签： c api z3

【解决方案1】：

看了HERE的源码，觉得里面有bug

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

下面的if

if (p == "rlimit")

应该是

else if (p == "rlimit")

为了避免错误的错误。

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

【讨论】：

谢谢@LPs，这正是答案。
再次感谢@LPS。但是，还有一个问题要问你是否知道，超时的配置似乎不起作用。在一个示例中，我将超时设置为“1u”（1 毫秒），添加一些约束（似乎以“1u”毫秒失败）并等待未知结果，但是，它得到了 68.7 秒的 sat 结果，来自计算Z3_check_and_get_model()之前和Z3_check_and_get_model()之后的时间差。
@user2940648 我不是 Z3 专家。我找到了THIS。也许能帮上忙。
@LPs，我知道这个页面，但和我的不一样。还是谢谢。
在您的问题中，您指的是 Z3 的不稳定分支。此分支不再使用，已从 GitHub 中删除。所有新的开发都直接进入主分支，所以在继续之前一定要切换到那个。