我创建了一个自定义理论插件，目前它什么都不做。回调都已实现并注册，但它们只是返回。然后，我使用 Z3_parse_smtlib2_string 读入了一堆声明常量、声明乐趣和断言，并将生成的 ast 传递给 Z3_assert_cnstr。随后对 Z3_check_and_get_model 的调用失败并出现以下错误：
没有为用户理论设置 mk_fresh_ext_data 回调，您必须使用 Z3_theory_set_mk_fresh_ext_data_callback
据我所知， Z3_theory_set_mk_fresh_ext_data_callback 不存在。
使用相同的字符串，但没有注册理论插件， Z3_check_and_get_model 返回 sat 并按预期提供模型。
我正在使用版本 4 和 Linux 64 位库。
完整的例子在这里： http: //pastebin.com/hLJ8hFf1
问题在于基于模型的量词实例化模块 (MBQI)。该模块尝试创建主逻辑引擎的副本。要创建副本，Z3 必须复制每个理论插件。它可以为所有内置理论做到这一点，但不适用于外部理论。
原始的理论插件 API 不支持复制自身，因为它是在 MBQI 模块之前实现的。APIZ3_theory_set_mk_fresh_ext_data_callback就是为此而生的。但是，由于多种原因，它还没有被曝光。主要问题是 Z3 4.0 有一个新的求解器 API。当前的理论插件 API 与新的求解器 API 不兼容。我们正在研究整合它们的方法。在 Z3 4.0 中，理论插件仅适用于旧的（已弃用的）求解器 API。
为避免您描述的问题，您只需禁用 MBQI 模块。您可以通过MBQI=false在创建时设置来做到这一点Z3_context。在 C 中，您可以使用以下代码片段来执行此操作。
Z3_config cfg;
Z3_context ctx;
cfg = Z3_mk_config();
Z3_set_param_value(cfg, "MBQI", "false");
ctx = Z3_mk_context(cfg);
这也解释了为什么您的插件适用于无量词公式。MBQI 模块不用于此类公式。