Усеченные целые числа, подобные C, в SMT-LIB 2

Question

Я передаю символьный вывод механизма символьного исполнения в Z3 в формате SMT-LIB 2.Мне нужно, чтобы оно усекало целые числа, как если бы они были в C. Чтобы (assert (= 1 (/ 3 2))) было бы SAT.

В этих формулах также могут быть числа с плавающей запятой, поэтому не все деления должны усекаться.Просто деление целых.

Как это сделать?

Answer 1

Целочисленное деление просто называется div:

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

Это дает:

sat