diff options
Diffstat (limited to 'src/theory/arith/theory_arith.cpp')
| -rw-r--r-- | src/theory/arith/theory_arith.cpp | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 577aa0e6c..2e2a99174 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -139,8 +139,8 @@ TrustNode TheoryArith::ppRewriteEq(TNode atom) return TrustNode::null(); } Assert(atom[0].getType().isReal()); - Node leq = NodeBuilder<2>(kind::LEQ) << atom[0] << atom[1]; - Node geq = NodeBuilder<2>(kind::GEQ) << atom[0] << atom[1]; + Node leq = NodeBuilder(kind::LEQ) << atom[0] << atom[1]; + Node geq = NodeBuilder(kind::GEQ) << atom[0] << atom[1]; Node rewritten = Rewriter::rewrite(leq.andNode(geq)); Debug("arith::preprocess") << "arith::preprocess() : returning " << rewritten << endl; @@ -161,7 +161,8 @@ Theory::PPAssertStatus TheoryArith::ppAssert( return d_internal->ppAssert(tin, outSubstitutions); } -void TheoryArith::ppStaticLearn(TNode n, NodeBuilder<>& learned) { +void TheoryArith::ppStaticLearn(TNode n, NodeBuilder& learned) +{ d_internal->ppStaticLearn(n, learned); } |