diff options
Diffstat (limited to 'src/theory/arith/infer_bounds.cpp')
| -rw-r--r-- | src/theory/arith/infer_bounds.cpp | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/src/theory/arith/infer_bounds.cpp b/src/theory/arith/infer_bounds.cpp index aae9bae62..21f698e45 100644 --- a/src/theory/arith/infer_bounds.cpp +++ b/src/theory/arith/infer_bounds.cpp @@ -163,9 +163,7 @@ Node InferBoundsResult::getLiteral() const{ Assert(getValue().infinitesimalSgn() >= 0); k = boundIsRational() ? kind::GEQ : kind::GT; } - Node atom = nm->mkNode(k, getTerm(), qnode); - Node lit = Rewriter::rewrite(atom); - return lit; + return nm->mkNode(k, getTerm(), qnode); } /* If there is a bound, this is a node that explains the bound. */ |