mkArithDiv

open fun <T : KArithSort> mkArithDiv(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

Create an Int/Real arithmetic division expression.

Note for Int division:

when rhs is positive, (div lhs) is the floor (round toward zero) of the rational number lhs/rhs

when rhs is negative, (div lhs) is the ceiling (round toward positive infinity) of the rational number lhs/rhs

For example: 47 div 13 = 3 47 div -13 = -3 -47 div 13 = -4 -47 div -13 = 4