diff options
Diffstat (limited to 'src/printer/smt2/smt2_printer.cpp')
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 013288880..0d3bab3d0 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -195,7 +195,8 @@ void Smt2Printer::toStream(std::ostream& out, case roundTowardNegative : out << "roundTowardNegative"; break; case roundTowardZero : out << "roundTowardZero"; break; default : - Unreachable("Invalid value of rounding mode constant (%d)",n.getConst<RoundingMode>()); + Unreachable() << "Invalid value of rounding mode constant (" + << n.getConst<RoundingMode>() << ")"; } break; case kind::CONST_BOOLEAN: @@ -982,7 +983,7 @@ void Smt2Printer::toStream(std::ostream& out, force_child_type[1] = NodeManager::currentNM()->mkSetType( elemType ); }else{ // APPLY_UF, APPLY_CONSTRUCTOR, etc. - Assert( n.hasOperator() ); + Assert(n.hasOperator()); TypeNode opt = n.getOperator().getType(); if (n.getKind() == kind::APPLY_CONSTRUCTOR) { @@ -996,7 +997,7 @@ void Smt2Printer::toStream(std::ostream& out, opt = TypeNode::fromType(dt[ci].getSpecializedConstructorType(tn)); } } - Assert( opt.getNumChildren() == n.getNumChildren() + 1 ); + Assert(opt.getNumChildren() == n.getNumChildren() + 1); for(size_t i = 0; i < n.getNumChildren(); ++i ) { force_child_type[i] = opt[i]; } @@ -1350,7 +1351,7 @@ void Smt2Printer::toStream(std::ostream& out, const UnsatCore& core) const { out << "(" << std::endl; SmtEngine * smt = core.getSmtEngine(); - Assert( smt!=NULL ); + Assert(smt != NULL); for(UnsatCore::const_iterator i = core.begin(); i != core.end(); ++i) { std::string name; if (smt->getExpressionName(*i,name)) { |