Z3 选项 hi_div0 是什么？

Question

Z3 选项 hi_div0 是什么意思？我找不到任何文档。

该选项如何影响性能以及它如何影响语义？

Answer 1

hi_div0 代表“被零除的硬件解释。启用后，这意味着被零除具有具体值而不是未解释的值（以及余数）。参见例如 bv_rewriter，它定义了有符号除法的值；其他值在同一文件中更靠下。