【发布时间】：2020-01-19 22:14:23
【问题描述】：
我将符号执行引擎的符号输出以 SMT-LIB 2 格式传递给 Z3。我需要它来截断整数，就像它们在 C 中一样。所以(assert (= 1 (/ 3 2))) 将是SAT。
这些公式也可能有浮点数，因此并非所有除法都应截断。只是整数的划分。
如何做到这一点？
【问题讨论】：
【发布时间】：2020-01-19 22:14:23
【问题描述】：
整数除法简称为div：
(assert (= 1 (div 3 2)))
(check-sat)
这会产生：
sat
【讨论】：