Skip to content

Commit 11d1c9b

Browse files
Princess: Add a comment about divWithSpecialZero
1 parent 61f810d commit 11d1c9b

File tree

1 file changed

+3
-0
lines changed

1 file changed

+3
-0
lines changed

src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -135,6 +135,9 @@ protected IExpression multiply(IExpression number1, IExpression number2) {
135135

136136
@Override
137137
protected IExpression divide(IExpression number1, IExpression number2) {
138+
// SMT-LIB allows division by zero, so we use divWithSpecialZero here.
139+
// If the divisor is zero, divWithSpecialZero will evaluate to a unary UF `ratDivZero`,
140+
// otherwise it is the normal division
138141
return Rationals.divWithSpecialZero(toType(number1), toType(number2));
139142
}
140143

0 commit comments

Comments
 (0)