From 82da3493eef569e40720197efd712980ccbfa8b3 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 6 Jun 2019 13:11:32 -0700
Subject: [PATCH] fix printing of recursive defs

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/ast_smt2_pp.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp
index ceeab30ff..15c4cbb5c 100644
--- a/src/ast/ast_smt2_pp.cpp
+++ b/src/ast/ast_smt2_pp.cpp
@@ -1188,7 +1188,7 @@ public:
         format * args[2];
         args[0] = r1;
         args[1] = r2;
-        r = mk_seq1<format**, f2f>(m(), args, args+2, f2f(), "define-rec-funs");
+        r = mk_seq1<format**, f2f>(m(), args, args+2, f2f(), "define-funs-rec");
     }
 
 
@@ -1308,7 +1308,7 @@ std::ostream & ast_smt2_pp_recdefs(std::ostream & out, vector<std::pair<func_dec
     smt2_printer pr(env, p);
     pr(funs, r);
     pp(out, r.get(), m, p);
-    return out;
+    return out << "\n";
 }