0

我将符号执行引擎的符号输出以 SMT-LIB 2 格式传递给 Z3。我需要它来截断整数，就像它们在 C 中一样。所以那(assert (= 1 (/ 3 2)))将是SAT.

这些公式也可能有浮点数，因此并非所有除法都应截断。只是整数的划分。

如何做到这一点？

4

1 回答 1

2

整数除法简称div：

(assert (= 1 (div 3 2)))
(check-sat)

这会产生：

sat
于 2019-09-19T01:04:43.110 回答