From 437a545c3b608b86ce0a8c58e55c916305b2672e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 6 Dec 2013 13:12:35 -0800
Subject: [PATCH] fix pretty printer

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/opt_context.cpp | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index acbd8293d..e3d4a555e 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -301,7 +301,9 @@ namespace opt {
         free_func_visitor(ast_manager& m): m(m) {}
         void operator()(var * n)        { }
         void operator()(app * n)        { 
-            m_funcs.insert(n->get_decl()); 
+            if (n->get_family_id() == null_family_id) {
+                m_funcs.insert(n->get_decl()); 
+            }
             sort* s = m.get_sort(n);
             if (s->get_family_id() == null_family_id) {
                 m_sorts.insert(s);
@@ -397,6 +399,7 @@ namespace opt {
                 break;
             }
         }        
+        out << "(optimize)\n"; 
         return out.str();
     }