diff --git a/trunk/source/Library-SmtLibUtils/src/de/uni_freiburg/informatik/ultimate/lib/smtlibutils/quantifier/DualJunctionDml.java b/trunk/source/Library-SmtLibUtils/src/de/uni_freiburg/informatik/ultimate/lib/smtlibutils/quantifier/DualJunctionDml.java
index 4a16ec5fc5e..57e4628522a 100644
--- a/trunk/source/Library-SmtLibUtils/src/de/uni_freiburg/informatik/ultimate/lib/smtlibutils/quantifier/DualJunctionDml.java
+++ b/trunk/source/Library-SmtLibUtils/src/de/uni_freiburg/informatik/ultimate/lib/smtlibutils/quantifier/DualJunctionDml.java
@@ -387,7 +387,7 @@ private EliminationResult applyDivEliminationWithSmallRemainder(final Eliminatio
 		final BigInteger aAsBigInteger = pmt.getA();
 		final BigInteger aTimesInverse = aAsBigInteger.multiply(pmt.getInverse());
 		final BigInteger nAsBigInteger = aTimesInverse.divide(pmt.getDivisor());
-		final BigInteger remainderG = aTimesInverse.mod(pmt.getDivisor());
+		final BigInteger remainderG = aTimesInverse.mod((pmt.getDivisor()).abs());
 		final BigInteger absRemainderG = remainderG.abs();
 		final int absIntRemainderG = absRemainderG.intValue();
 		final Term nAsTerm = SmtUtils.constructIntegerValue(mScript, SmtSortUtils.getIntSort(mScript), nAsBigInteger);
@@ -435,6 +435,9 @@ private EliminationResult applyDivEliminationWithSmallRemainder(final Eliminatio
 			Term divConjunctSub = Substitution.apply(mMgdScript, subJunct, pmt.getContainingDualJunct());
 			termJunctSubstList.add(divConjunctSub);
 		}
+		//QuantifierUtils.applyDualFiniteConnective
+		//final Term termJunctSubst = QuantifierUtils.applyDualFiniteConnective(mScript, inputEt.getQuantifier(),
+			//	termJunctSubstList);
 		final Term termJunctSubst = QuantifierUtils.applyCorrespondingFiniteConnective(mScript, inputEt.getQuantifier(),
 				termJunctSubstList);
 		//final Map<Term, Term> sub3 = new HashMap<Term, Term>();