diff options
| author | Tim King <taking@cs.nyu.edu> | 2010-07-07 16:23:22 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2010-07-07 16:23:22 +0000 |
| commit | 3b017f6c69c9a32e229fe3a9e8b5aeacbfc35a47 (patch) | |
| tree | f8e34bd16a03a779113cee7943299039246e4cae /src/theory/arith/arith_rewriter.h | |
| parent | 26c1b20086b26da79d938057b7761de95fabf731 (diff) | |
Fixes arith rewriter to allow for division by a constant. It previously only allowed for a constant divided by a constant.
Diffstat (limited to 'src/theory/arith/arith_rewriter.h')
| -rw-r--r-- | src/theory/arith/arith_rewriter.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h index 38c72d38d..a76ee6e61 100644 --- a/src/theory/arith/arith_rewriter.h +++ b/src/theory/arith/arith_rewriter.h @@ -103,7 +103,7 @@ private: Node multPnfByNonZero(TNode pnf, Rational& q); - Node rewriteConstantDiv(TNode t); + Node rewriteDivByConstant(TNode t); void sortAndCombineCoefficients(std::vector<Node>& pnfs); |