mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
remove debug code
This commit is contained in:
parent
372e8b3c49
commit
625874e66f
|
@ -62,14 +62,14 @@ class blast_term_ite_tactic : public tactic {
|
|||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
expr* c, *t, *e;
|
||||
if (!m.is_bool(args[i]) && m.is_ite(args[i], c, t, e)) {
|
||||
enable_trace("blast_term_ite");
|
||||
// enable_trace("blast_term_ite");
|
||||
TRACE("blast_term_ite", result = m.mk_app(f, num_args, args); tout << result << "\n";);
|
||||
expr_ref e1(m), e2(m);
|
||||
ptr_vector<expr> args1(num_args, args);
|
||||
args1[i] = t;
|
||||
++m_num_fresh;
|
||||
e1 = m.mk_app(f, num_args, args1.c_ptr());
|
||||
if (t == e) {
|
||||
if (m.are_equal(t,e)) {
|
||||
result = e1;
|
||||
return BR_REWRITE1;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue