diff options
Diffstat (limited to 'src/preprocessing/passes/real_to_int.cpp')
| -rw-r--r-- | src/preprocessing/passes/real_to_int.cpp | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp index 9e2170ffd..5c4539808 100644 --- a/src/preprocessing/passes/real_to_int.cpp +++ b/src/preprocessing/passes/real_to_int.cpp @@ -27,6 +27,7 @@ #include "theory/theory_model.h" #include "util/rational.h" +using namespace cvc5::kind; using namespace cvc5::theory; namespace cvc5 { @@ -78,6 +79,7 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& va { Assert(c.isConst()); coeffs.push_back(NodeManager::currentNM()->mkConst( + CONST_RATIONAL, Rational(c.getConst<Rational>().getDenominator()))); } } @@ -97,7 +99,8 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& va Node s; if (c.isNull()) { - c = cc.isNull() ? NodeManager::currentNM()->mkConst(Rational(1)) + c = cc.isNull() ? NodeManager::currentNM()->mkConst( + CONST_RATIONAL, Rational(1)) : cc; } else @@ -131,14 +134,15 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& va } Node sumt = sum.empty() - ? NodeManager::currentNM()->mkConst(Rational(0)) + ? NodeManager::currentNM()->mkConst(CONST_RATIONAL, + Rational(0)) : (sum.size() == 1 ? sum[0] : NodeManager::currentNM()->mkNode(kind::PLUS, sum)); ret = NodeManager::currentNM()->mkNode( ret_lit.getKind(), sumt, - NodeManager::currentNM()->mkConst(Rational(0))); + NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0))); if (!ret_pol) { ret = ret.negate(); |