From 44c417904b268c6bbb175082c81f58c0ada1a422 Mon Sep 17 00:00:00 2001
From: Doug Woos <doug.woos@gmail.com>
Date: Wed, 1 Feb 2017 16:21:01 -0800
Subject: [PATCH] correctly pretty-print

---
 src/tactic/sine_filter.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/tactic/sine_filter.cpp b/src/tactic/sine_filter.cpp
index 43c15bf74..059608b4c 100644
--- a/src/tactic/sine_filter.cpp
+++ b/src/tactic/sine_filter.cpp
@@ -26,6 +26,7 @@ Revision History:
 #include "var_subst.h"
 #include "ast_util.h"
 #include "obj_pair_hashtable.h"
+#include "ast_pp.h"
 
 class sine_tactic : public tactic {
 
@@ -121,7 +122,7 @@ private:
                     app *a = to_app(curr);
                     func_decl *f = a->get_decl();
                     if (!consts.contains(f)) {
-                        TRACE("sine", tout << f; tout << "\n";);
+                        TRACE("sine", tout << mk_pp(f, m) << "\n";);
                         p_matched = false;
                         next_consts.push_back(f);
                         break;