diff options
Diffstat (limited to 'src/printer/smt2/smt2_printer.cpp')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 13 |
1 files changed, 2 insertions, 11 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 03422c162..2b686441a 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -100,25 +100,16 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::BUILTIN: out << smtKindString(n.getConst<Kind>()); break; - case kind::CONST_INTEGER: { - Integer i = n.getConst<Integer>(); - if(i < 0) { - out << "(- " << -i << ')'; - } else { - out << i; - } - break; - } case kind::CONST_RATIONAL: { Rational r = n.getConst<Rational>(); if(r < 0) { - if(r.getDenominator() == 1) { + if(r.isIntegral()) { out << "(- " << -r << ')'; } else { out << "(- (/ " << (-r).getNumerator() << ' ' << (-r).getDenominator() << "))"; } } else { - if(r.getDenominator() == 1) { + if(r.isIntegral()) { out << r; } else { out << "(/ " << r.getNumerator() << ' ' << r.getDenominator() << ')'; |