From ce1c8f7be29f5c9bf4f22e1c697d4032e0828ee7 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Thu, 19 Oct 2017 17:01:10 -0400 Subject: [PATCH] remove debug code --- src/smt/theory_str.cpp | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 41d42c867..7e5685f9c 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -8889,8 +8889,6 @@ namespace smt { TRACE("str", tout << "backpropagate into " << mk_pp(var, m) << " = " << mk_pp(concat, m) << std::endl << "LHS ~= " << mk_pp(concat_lhs_str, m) << " RHS ~= " << mk_pp(concat_rhs_str, m) << std::endl;); - TRACE("str_enode_bug", tout << "backpropagate into " << mk_pp(var, m) << " = " << mk_pp(concat, m) << std::endl - << "LHS ~= " << mk_pp(concat_lhs_str, m) << " RHS ~= " << mk_pp(concat_rhs_str, m) << std::endl;); zstring lhsString, rhsString; u.str.is_string(concat_lhs_str, lhsString); u.str.is_string(concat_rhs_str, rhsString); @@ -8912,8 +8910,6 @@ namespace smt { } else { expr_ref lhs(mk_and(lhs_terms), m); expr_ref rhs(ctx.mk_eq_atom(concat, mk_string(concatString)), m); - TRACE("str_enode_bug", tout << "axiom LHS: " << mk_pp(lhs, m) << std::endl;); - TRACE("str_enode_bug", tout << "axiom RHS: " << mk_pp(rhs, m) << std::endl;); assert_implication(lhs, rhs); } backpropagation_occurred = true;