当十字光标没有找到反例时，它是否使用Z3求解器来证明我的合同成立？
文档表明，没有反例并不能保证该属性成立，但这只是因为翻译或建模可能不正确吗？
免责声明：我是CrossHair的主要贡献者(我只是使用堆栈溢出作为一种公共方式来记录我之前被问到的问题的答案(
除了建模不健全可能存在的许多问题外，CrossHair不提供此保证。
CrossHair是一个极其不完整的系统。在内部，对于每个后置条件，它都会生成三个可能的结果："已确认"、"已拒绝"one_answers"未知"；因此，没有输出并不表示对该语句进行了验证。
为什么CrossHair是这样工作的？两个原因：
- CrossHair为除最琐碎的情况外的所有情况生成"未知"。对于大多数开发人员来说，"未知"one_answers"已确认"之间的区别并不是很可行。(至少目前，重构代码以使其完全可由CrossHair探索是不可能的或丑陋的(然而，请注意，CrossHair在产生"未知"结果之前会尝试许多执行路径-结果仍然提供了一些证据来证明条件成立
- 随着时间的推移，已确认与未知的区别将非常不稳定。CrossHair的设计从一开始就是为了进化。平均而言，SMT解决方案会变得更好。CrossHair会变得更好。但两者都会变得更好平均；对于个别情况，两者都可能变得更糟。为了避免对已确认和未知回归的担忧，默认情况下隐藏了这种区别
最好将CrossHair视为解算器辅助的模糊测试程序。
话虽如此，如果你仍然想看看哪些属性是可确认的，你可以用一个特殊的"全部报告"选项请求这个输出：crosshair check --report_all [TARGET]。