Update the JavaDoc for Integer modulo

BaierD · BaierD · commit bf6bda3e40c0 · 2024-08-30T20:21:06.000+02:00
diff --git a/src/org/sosy_lab/java_smt/api/IntegerFormulaManager.java b/src/org/sosy_lab/java_smt/api/IntegerFormulaManager.java
@@ -27,7 +27,8 @@ public interface IntegerFormulaManager
 
   /**
    * Create a formula representing the modulo of two operands according to Boute's Euclidean
-   * definition.
+   * definition. The quotient (div numerator denominator) of the internal modulo calculation is
+   * floored for positive denominators and rounded up for negative denominators.
    *
    * <p>If the denominator evaluates to zero (modulo-by-zero), either directly as value or
    * indirectly via an additional constraint, then the solver is allowed to choose an arbitrary

Original file line number	Diff line number	Diff line change
`@@ -27,7 +27,8 @@ public interface IntegerFormulaManager`
`27`	`27`
`28`	`28`	`/**`
`29`	`29`	`* Create a formula representing the modulo of two operands according to Boute's Euclidean`
`30`		`- * definition.`
	`30`	`+ * definition. The quotient (div numerator denominator) of the internal modulo calculation is`
	`31`	`+ * floored for positive denominators and rounded up for negative denominators.`
`31`	`32`	`*`
`32`	`33`	`* <p>If the denominator evaluates to zero (modulo-by-zero), either directly as value or`
`33`	`34`	`* indirectly via an additional constraint, then the solver is allowed to choose an arbitrary`