diff options
Diffstat (limited to 'src/printer/cvc/cvc_printer.cpp')
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 0d47c9c6c..8d76a7332 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -484,15 +484,19 @@ static void toStream(std::ostream& out, const DefineFunctionCommand* c) throw() Expr func = c->getFunction(); const vector<Expr>& formals = c->getFormals(); Expr formula = c->getFormula(); - out << func << " : " << func.getType() << " = LAMBDA("; - vector<Expr>::const_iterator i = formals.begin(); - while(i != formals.end()) { - out << (*i) << ":" << (*i).getType(); - if(++i != formals.end()) { - out << ", "; + out << func << " : " << func.getType() << " = "; + if(formals.size() > 0) { + out << "LAMBDA("; + vector<Expr>::const_iterator i = formals.begin(); + while(i != formals.end()) { + out << (*i) << ":" << (*i).getType(); + if(++i != formals.end()) { + out << ", "; + } } + out << "): "; } - out << "): " << formula << ";"; + out << formula << ";"; } static void toStream(std::ostream& out, const DeclareTypeCommand* c) throw() { |