mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-18 20:03:38 +00:00
Code Activity

correctly pretty-print

Browse source
This commit is contained in:
Doug Woos 2017-02-01 16:21:01 -08:00
parent a147e2bc35
commit 44c417904b
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/tactic/sine_filter.cpp
View file

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