使用NuXMV进行BMC验证前是否需安装Zchaff？实操存疑

• 刚安装NuXMV准备做有界模型验证（BMC），看用户手册说NuXMV没包含Zchaff或minisat，疑惑得先装这俩才能开展工作，但用msat_check_ltlspec_bmc指令跑简单模型居然成功了，这就搞不懂了。
• 核心原因很直接：NuXMV内置了MathSAT求解器，你用的msat_check_ltlspec_bmc指令就是专门调用这个内置求解器的，完全不需要额外安装Zchaff或minisat。
• 手册里提到的Zchaff/minisat是给不带msat_前缀的BMC指令（比如check_ltlspec_bmc）准备的可选依赖，这类指令需要外部SAT求解器支持，但你选的指令走内置求解器路线，自然不用额外安装。

你的简单模型与运行结果说明 #

• 简单SMV模型：定义变量a初始值为0，转换规则设为next(a) = a + 1，待验证的LTL属性为G(a < 3)（即全局状态下a始终小于3）。
• 运行结果：验证过程顺利完成，输出显示该LTL属性成立，同时给出了验证使用的界以及MathSAT求解器的运行相关信息。

内容的提问来源于stack exchange，提问作者yayi-mei