mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 04:43:39 +00:00
Code Activity

add logging

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-06-28 16:10:15 -07:00
parent 12e7b4c3d6
commit fd8ee34564
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_user_propagator.cpp
View file

@ -20,6 +20,7 @@ Author:
#include "smt/theory_bv.h" #include "smt/theory_bv.h"
#include "smt/theory_user_propagator.h" #include "smt/theory_user_propagator.h"
#include "smt/smt_context.h" #include "smt/smt_context.h"
#include "ast/ast_ll_pp.h"
using namespace smt; using namespace smt;
@ -49,6 +50,7 @@ void theory_user_propagator::add_expr(expr* term, bool ensure_enode) {
expr_ref r(m); expr_ref r(m);
expr* e = term; expr* e = term;
ctx.get_rewriter()(e, r); ctx.get_rewriter()(e, r);
TRACE("user_propagate", tout << "add " << mk_bounded_pp(e, m) << "\n");
if (r != e) { if (r != e) {
r = m.mk_fresh_const("aux-expr", e->get_sort()); r = m.mk_fresh_const("aux-expr", e->get_sort());
expr_ref eq(m.mk_eq(r, e), m); expr_ref eq(m.mk_eq(r, e), m);