diff options
| author | Tim King <taking@cs.nyu.edu> | 2012-12-14 21:07:00 -0500 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2012-12-14 21:07:00 -0500 |
| commit | cb3c0621a7d54325c8863d315ea7569fa70bdc10 (patch) | |
| tree | 610813d2c679d3dac3085c13817978e8c6dc533e /src/theory/arith/theory_arith.cpp | |
| parent | 282f757fd1c9a5277e9d7053e9a20d792c8b81b0 (diff) | |
| parent | 7d0625db683e06cc55b8ffa2f56a8b26e6bb7427 (diff) | |
Merging in patch from branch '1.0.x'.
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 f036e20fd..7f7ee3bb1 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -2060,10 +2060,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); |