Princess: Use total definition for division where a/0 is allowed

daniel-raffler · daniel-raffler · commit fec5a6164d1e · 2025-09-05T16:54:50.000+02:00
diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java
@@ -135,7 +135,7 @@ protected IExpression multiply(IExpression number1, IExpression number2) {
 
   @Override
   protected IExpression divide(IExpression number1, IExpression number2) {
-    return Rationals.div(toType(number1), toType(number2));
+    return Rationals.divWithSpecialZero(toType(number1), toType(number2));
   }
 
   @Override

Original file line number	Diff line number	Diff line change
`@@ -135,7 +135,7 @@ protected IExpression multiply(IExpression number1, IExpression number2) {`
`135`	`135`
`136`	`136`	`@Override`
`137`	`137`	`protected IExpression divide(IExpression number1, IExpression number2) {`
`138`		`- return Rationals.div(toType(number1), toType(number2));`
	`138`	`+ return Rationals.divWithSpecialZero(toType(number1), toType(number2));`
`139`	`139`	`}`
`140`	`140`
`141`	`141`	`@Override`