diff options
| author | Tim King <taking@cs.nyu.edu> | 2012-12-14 20:09:54 -0500 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2012-12-14 20:09:54 -0500 |
| commit | edf971e2934367d160830a35e97a2e664e742b28 (patch) | |
| tree | 07715a33a93a8edf2aec5afd71f71fb9b1c7d012 /src/theory/arith/theory_arith.cpp | |
| parent | 5d0d0b56d1383f1ad4027d8e6dc739c12cacced8 (diff) | |
Changing the rewriter to use Boute's Euclidean definition of division.
Diffstat (limited to 'src/theory/arith/theory_arith.cpp')
| -rw-r--r-- | src/theory/arith/theory_arith.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 6ec6c7090..c2c005767 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -2009,10 +2009,10 @@ DeltaRational TheoryArith::getDeltaValue(TNode n) const throw (DeltaRationalExce if(n.getKind() == kind::DIVISION_TOTAL){ res = numer / denom; }else if(n.getKind() == kind::INTS_DIVISION_TOTAL){ - res = Rational(numer.floorDivideQuotient(denom)); + res = Rational(numer.euclidianDivideQuotient(denom)); }else{ Assert(n.getKind() == kind::INTS_MODULUS_TOTAL); - res = Rational(numer.floorDivideRemainder(denom)); + res = Rational(numer.euclidianDivideRemainder(denom)); } if(isSetup(n)){ ArithVar var = d_arithvarNodeMap.asArithVar(n); |