Corrected div-method for negative divisors, in one line: ...mod(divis…

…or.abs())
ultimate-pa · Feb 23, 2023 · dde5649 · dde5649
1 parent 63fe0d5
commit dde5649
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/...s/src/de/uni_freiburg/informatik/ultimate/lib/smtlibutils/quantifier/DualJunctionDml.java b/...s/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>();