From 51e459d02b153ec7d130fc2572b72d89a70fec8a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Mar 2020 10:46:03 -0700 Subject: [PATCH] fix #3294 Signed-off-by: Nikolaj Bjorner --- src/ackermannization/ackermannize_bv_tactic.cpp | 1 - src/ast/rewriter/rewriter_def.h | 13 +++++++++---- src/ast/rewriter/th_rewriter.cpp | 3 +++ src/muz/fp/horn_tactic.cpp | 3 --- src/nlsat/tactic/nlsat_tactic.cpp | 3 --- src/qe/qe_lite.cpp | 3 --- src/qe/qe_tactic.cpp | 3 --- src/smt/tactic/ctx_solver_simplify_tactic.cpp | 2 -- src/smt/tactic/smt_tactic.cpp | 2 +- src/tactic/aig/aig_tactic.cpp | 3 --- src/tactic/arith/card2bv_tactic.cpp | 3 --- src/tactic/arith/degree_shift_tactic.cpp | 2 -- src/tactic/arith/diff_neq_tactic.cpp | 3 --- src/tactic/arith/eq2bv_tactic.cpp | 3 --- src/tactic/arith/factor_tactic.cpp | 3 --- src/tactic/arith/fix_dl_var_tactic.cpp | 3 --- src/tactic/arith/fm_tactic.cpp | 2 -- src/tactic/arith/lia2card_tactic.cpp | 4 ---- src/tactic/arith/lia2pb_tactic.cpp | 3 --- src/tactic/arith/nla2bv_tactic.cpp | 2 -- src/tactic/arith/pb2bv_tactic.cpp | 3 --- src/tactic/arith/propagate_ineqs_tactic.cpp | 3 +-- src/tactic/arith/purify_arith_tactic.cpp | 3 --- src/tactic/arith/recover_01_tactic.cpp | 3 +-- src/tactic/bv/bv_bound_chk_tactic.cpp | 5 ----- src/tactic/bv/bv_size_reduction_tactic.cpp | 2 -- src/tactic/bv/bvarray2uf_tactic.cpp | 4 ---- src/tactic/bv/dt2bv_tactic.cpp | 2 -- src/tactic/bv/elim_small_bv_tactic.cpp | 3 --- src/tactic/bv/max_bv_sharing_tactic.cpp | 3 --- src/tactic/core/blast_term_ite_tactic.cpp | 3 --- src/tactic/core/cofactor_term_ite_tactic.cpp | 3 --- src/tactic/core/ctx_simplify_tactic.cpp | 2 -- src/tactic/core/der_tactic.cpp | 4 ---- src/tactic/core/distribute_forall_tactic.cpp | 3 --- src/tactic/core/elim_term_ite_tactic.cpp | 3 --- src/tactic/core/injectivity_tactic.cpp | 1 - src/tactic/core/nnf_tactic.cpp | 3 --- src/tactic/core/occf_tactic.cpp | 3 --- src/tactic/core/pb_preprocess_tactic.cpp | 3 +-- src/tactic/core/propagate_values_tactic.cpp | 3 +-- src/tactic/core/reduce_args_tactic.cpp | 2 -- src/tactic/core/simplify_tactic.cpp | 2 -- src/tactic/core/solve_eqs_tactic.cpp | 3 --- src/tactic/core/split_clause_tactic.cpp | 1 - src/tactic/core/tseitin_cnf_tactic.cpp | 3 --- src/tactic/fpa/fpa2bv_tactic.cpp | 2 -- src/tactic/goal.cpp | 8 ++++++-- src/tactic/goal.h | 2 +- src/tactic/sine_filter.cpp | 2 +- src/tactic/sls/sls_tactic.cpp | 3 --- src/tactic/tactic.cpp | 2 ++ src/tactic/ufbv/macro_finder_tactic.cpp | 3 --- src/tactic/ufbv/quasi_macros_tactic.cpp | 3 --- src/tactic/ufbv/ufbv_rewriter_tactic.cpp | 3 --- 55 files changed, 27 insertions(+), 138 deletions(-) diff --git a/src/ackermannization/ackermannize_bv_tactic.cpp b/src/ackermannization/ackermannize_bv_tactic.cpp index 88fde3f83..dcf6a7c59 100644 --- a/src/ackermannization/ackermannize_bv_tactic.cpp +++ b/src/ackermannization/ackermannize_bv_tactic.cpp @@ -59,7 +59,6 @@ public: resg->inc_depth(); TRACE("goal", resg->display(tout << "out\n");); - SASSERT(resg->is_well_sorted()); } diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index 5cd3ec239..c80a0b2ca 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -527,12 +527,18 @@ void rewriter_tpl::process_quantifier(quantifier * q, frame & fr) { TRACE("reduce_quantifier_bug", tout << "rewrite patterns\n";); expr * const * np = it + 1; expr * const * nnp = np + num_pats; + unsigned j = 0; for (unsigned i = 0; i < num_pats; i++) if (m_manager.is_pattern(np[i])) - new_pats[i] = np[i]; + new_pats[j++] = np[i]; + new_pats.shrink(j); + num_pats = j; + j = 0; for (unsigned i = 0; i < num_no_pats; i++) if (m_manager.is_pattern(nnp[i])) - new_no_pats[i] = nnp[i]; + new_no_pats[j++] = nnp[i]; + new_no_pats.shrink(j); + num_no_pats = j; } if (ProofGen) { quantifier_ref new_q(m().update_quantifier(q, num_pats, new_pats.c_ptr(), num_no_pats, new_no_pats.c_ptr(), new_body), m()); @@ -547,8 +553,7 @@ void rewriter_tpl::process_quantifier(quantifier * q, frame & fr) { if (m_cfg.reduce_quantifier(new_q, new_body, new_pats.c_ptr(), new_no_pats.c_ptr(), m_r, pr2)) { m_pr = m().mk_transitivity(m_pr, pr2); } - TRACE("reduce_quantifier_bug", tout << "m_pr is_null: " << (m_pr.get() == 0) << "\n"; - if (m_pr) tout << mk_ismt2_pp(m_pr, m()) << "\n";); + TRACE("reduce_quantifier_bug",if (m_pr) tout << mk_ismt2_pp(m_pr, m()) << "\n"; else tout << "m_pr is_null\n";); result_pr_stack().shrink(fr.m_spos); result_pr_stack().push_back(m_pr); } diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 177a9f442..d411f5c40 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -718,6 +718,9 @@ struct th_rewriter_cfg : public default_rewriter_cfg { new_body); TRACE("reduce_quantifier", tout << mk_ismt2_pp(old_q, m()) << "\n----->\n" << mk_ismt2_pp(q1, m()) << "\n";); SASSERT(is_well_sorted(m(), q1)); + if (m().proofs_enabled() && q1 != old_q) { + p1 = m().mk_rewrite(old_q, q1); + } } SASSERT(m().get_sort(old_q) == m().get_sort(q1)); result = elim_unused_vars(m(), q1, params_ref()); diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp index 65be3e9ae..8fee59990 100644 --- a/src/muz/fp/horn_tactic.cpp +++ b/src/muz/fp/horn_tactic.cpp @@ -178,7 +178,6 @@ class horn_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result) { - SASSERT(g->is_well_sorted()); tactic_report report("horn", *g); bool produce_proofs = g->proofs_enabled(); @@ -296,8 +295,6 @@ class horn_tactic : public tactic { // subgoal is unchanged. break; } - TRACE("horn", g->display(tout);); - SASSERT(g->is_well_sorted()); } void bind_variables(expr_ref& f) { diff --git a/src/nlsat/tactic/nlsat_tactic.cpp b/src/nlsat/tactic/nlsat_tactic.cpp index 5016c951b..10286520a 100644 --- a/src/nlsat/tactic/nlsat_tactic.cpp +++ b/src/nlsat/tactic/nlsat_tactic.cpp @@ -133,7 +133,6 @@ class nlsat_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result) { - SASSERT(g->is_well_sorted()); tactic_report report("nlsat", *g); if (g->is_decided()) { @@ -191,8 +190,6 @@ class nlsat_tactic : public tactic { g->inc_depth(); result.push_back(g.get()); - TRACE("nlsat", g->display(tout);); - SASSERT(g->is_well_sorted()); } }; diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index aa96ce9ba..50f7985a0 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -2473,7 +2473,6 @@ public: void operator()(goal_ref const & g, goal_ref_buffer & result) override { - SASSERT(g->is_well_sorted()); tactic_report report("qe-lite", *g); proof_ref new_pr(m); expr_ref new_f(m); @@ -2504,8 +2503,6 @@ public: } g->inc_depth(); result.push_back(g.get()); - TRACE("qe", g->display(tout);); - SASSERT(g->is_well_sorted()); } void collect_statistics(statistics & st) const override { diff --git a/src/qe/qe_tactic.cpp b/src/qe/qe_tactic.cpp index db0543d4f..512679de0 100644 --- a/src/qe/qe_tactic.cpp +++ b/src/qe/qe_tactic.cpp @@ -49,7 +49,6 @@ class qe_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result) { - SASSERT(g->is_well_sorted()); tactic_report report("qe", *g); m_fparams.m_model = g->models_enabled(); proof_ref new_pr(m); @@ -74,8 +73,6 @@ class qe_tactic : public tactic { g->inc_depth(); g->elim_true(); result.push_back(g.get()); - TRACE("qe", g->display(tout);); - SASSERT(g->is_well_sorted()); } void collect_statistics(statistics & st) const { diff --git a/src/smt/tactic/ctx_solver_simplify_tactic.cpp b/src/smt/tactic/ctx_solver_simplify_tactic.cpp index bb6a66e58..80efcc048 100644 --- a/src/smt/tactic/ctx_solver_simplify_tactic.cpp +++ b/src/smt/tactic/ctx_solver_simplify_tactic.cpp @@ -83,7 +83,6 @@ protected: void reduce(goal& g) { - SASSERT(g.is_well_sorted()); TRACE("ctx_solver_simplify_tactic", g.display(tout);); expr_ref fml(m); tactic_report report("ctx-solver-simplify", g); @@ -125,7 +124,6 @@ protected: g.reset(); g.assert_expr(fml, nullptr, nullptr); IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "(ctx-solver-simplify :num-steps " << m_num_steps << ")\n";); - SASSERT(g.is_well_sorted()); } struct expr_pos { diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index 2dcd19c0d..116e1f793 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -150,8 +150,8 @@ public: goal_ref_buffer & result) override { try { IF_VERBOSE(10, verbose_stream() << "(smt.tactic start)\n";); - SASSERT(in->is_well_sorted()); ast_manager & m = in->m(); + tactic_report report("smt", *in); TRACE("smt_tactic", tout << this << "\nAUTO_CONFIG: " << fparams().m_auto_config << " HIDIV0: " << fparams().m_hi_div0 << " " << " PREPROCESS: " << fparams().m_preprocess << "\n"; tout << "RELEVANCY: " << fparams().m_relevancy_lvl << "\n"; diff --git a/src/tactic/aig/aig_tactic.cpp b/src/tactic/aig/aig_tactic.cpp index 720c799e0..7b80582fe 100644 --- a/src/tactic/aig/aig_tactic.cpp +++ b/src/tactic/aig/aig_tactic.cpp @@ -66,7 +66,6 @@ public: } void operator()(goal_ref const & g) { - SASSERT(g->is_well_sorted()); mk_aig_manager mk(*this, g->m()); if (m_aig_per_assertion) { @@ -86,7 +85,6 @@ public: m_aig_manager->max_sharing(r); m_aig_manager->to_formula(r, *(g.get())); } - SASSERT(g->is_well_sorted()); } void operator()(goal_ref const & g, goal_ref_buffer & result) override { @@ -94,7 +92,6 @@ public: tactic_report report("aig", *g); operator()(g); g->inc_depth(); - TRACE("aig", g->display(tout);); result.push_back(g.get()); } diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp index f68a6e082..3a2f0dabd 100644 --- a/src/tactic/arith/card2bv_tactic.cpp +++ b/src/tactic/arith/card2bv_tactic.cpp @@ -54,7 +54,6 @@ public: void operator()(goal_ref const & g, goal_ref_buffer & result) override { TRACE("card2bv-before", g->display(tout);); - SASSERT(g->is_well_sorted()); result.reset(); tactic_report report("card2bv", *g); th_rewriter rw1(m, m_params); @@ -92,8 +91,6 @@ public: g->inc_depth(); result.push_back(g.get()); - TRACE("card2bv", g->display(tout);); - SASSERT(g->is_well_sorted()); } void cleanup() override { diff --git a/src/tactic/arith/degree_shift_tactic.cpp b/src/tactic/arith/degree_shift_tactic.cpp index 403f0a317..f90b94f27 100644 --- a/src/tactic/arith/degree_shift_tactic.cpp +++ b/src/tactic/arith/degree_shift_tactic.cpp @@ -222,7 +222,6 @@ class degree_shift_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result) { - SASSERT(g->is_well_sorted()); m_produce_proofs = g->proofs_enabled(); m_produce_models = g->models_enabled(); tactic_report report("degree_shift", *g); @@ -268,7 +267,6 @@ class degree_shift_tactic : public tactic { g->add(mc.get()); result.push_back(g.get()); TRACE("degree_shift", g->display(tout); if (mc) mc->display(tout);); - SASSERT(g->is_well_sorted()); } }; diff --git a/src/tactic/arith/diff_neq_tactic.cpp b/src/tactic/arith/diff_neq_tactic.cpp index a7907b24a..e91d22b6a 100644 --- a/src/tactic/arith/diff_neq_tactic.cpp +++ b/src/tactic/arith/diff_neq_tactic.cpp @@ -314,7 +314,6 @@ class diff_neq_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result) { - SASSERT(g->is_well_sorted()); m_produce_models = g->models_enabled(); result.reset(); tactic_report report("diff-neq", *g); @@ -339,8 +338,6 @@ class diff_neq_tactic : public tactic { } g->inc_depth(); result.push_back(g.get()); - TRACE("diff_neq", g->display(tout);); - SASSERT(g->is_well_sorted()); } }; diff --git a/src/tactic/arith/eq2bv_tactic.cpp b/src/tactic/arith/eq2bv_tactic.cpp index f44029d70..9361ec2fb 100644 --- a/src/tactic/arith/eq2bv_tactic.cpp +++ b/src/tactic/arith/eq2bv_tactic.cpp @@ -151,7 +151,6 @@ public: } void operator()(goal_ref const & g, goal_ref_buffer & result) override { - SASSERT(g->is_well_sorted()); m_trail.reset(); m_fd.reset(); m_max.reset(); @@ -209,8 +208,6 @@ public: g->inc_depth(); g->add(mc1.get()); result.push_back(g.get()); - TRACE("pb", g->display(tout);); - SASSERT(g->is_well_sorted()); } diff --git a/src/tactic/arith/factor_tactic.cpp b/src/tactic/arith/factor_tactic.cpp index 0ad246852..18f11906b 100644 --- a/src/tactic/arith/factor_tactic.cpp +++ b/src/tactic/arith/factor_tactic.cpp @@ -258,7 +258,6 @@ class factor_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result) { - SASSERT(g->is_well_sorted()); tactic_report report("factor", *g); bool produce_proofs = g->proofs_enabled(); @@ -276,8 +275,6 @@ class factor_tactic : public tactic { } g->inc_depth(); result.push_back(g.get()); - TRACE("factor", g->display(tout);); - SASSERT(g->is_well_sorted()); } }; diff --git a/src/tactic/arith/fix_dl_var_tactic.cpp b/src/tactic/arith/fix_dl_var_tactic.cpp index 2019d29fb..36679b1dc 100644 --- a/src/tactic/arith/fix_dl_var_tactic.cpp +++ b/src/tactic/arith/fix_dl_var_tactic.cpp @@ -248,7 +248,6 @@ class fix_dl_var_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result) { - SASSERT(g->is_well_sorted()); tactic_report report("fix-dl-var", *g); bool produce_proofs = g->proofs_enabled(); m_produce_models = g->models_enabled(); @@ -284,8 +283,6 @@ class fix_dl_var_tactic : public tactic { g->inc_depth(); } result.push_back(g.get()); - TRACE("fix_dl_var", g->display(tout);); - SASSERT(g->is_well_sorted()); } }; diff --git a/src/tactic/arith/fm_tactic.cpp b/src/tactic/arith/fm_tactic.cpp index 22b73874f..20cde5e21 100644 --- a/src/tactic/arith/fm_tactic.cpp +++ b/src/tactic/arith/fm_tactic.cpp @@ -1550,7 +1550,6 @@ class fm_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result) { - SASSERT(g->is_well_sorted()); tactic_report report("fm", *g); fail_if_proof_generation("fm", g); m_produce_models = g->models_enabled(); @@ -1604,7 +1603,6 @@ class fm_tactic : public tactic { reset_constraints(); result.push_back(m_new_goal.get()); TRACE("fm", m_new_goal->display(tout);); - SASSERT(m_new_goal->is_well_sorted()); } void display_constraints(std::ostream & out, constraints const & cs) const { diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp index b5f7d9739..4c64c0a30 100644 --- a/src/tactic/arith/lia2card_tactic.cpp +++ b/src/tactic/arith/lia2card_tactic.cpp @@ -170,13 +170,11 @@ public: } void operator()(goal_ref const & g, goal_ref_buffer & result) override { - SASSERT(g->is_well_sorted()); m_bounds.reset(); m_mc.reset(); expr_ref_vector axioms(m); expr_safe_replace rep(m); - TRACE("pb", g->display(tout);); tactic_report report("lia2card", *g); bound_manager bounds(m); @@ -218,8 +216,6 @@ public: if (m_mc) g->add(m_mc.get()); g->inc_depth(); result.push_back(g.get()); - TRACE("pb", g->display(tout);); - SASSERT(g->is_well_sorted()); m_bounds.reset(); } diff --git a/src/tactic/arith/lia2pb_tactic.cpp b/src/tactic/arith/lia2pb_tactic.cpp index 08f588829..86e11668f 100644 --- a/src/tactic/arith/lia2pb_tactic.cpp +++ b/src/tactic/arith/lia2pb_tactic.cpp @@ -185,7 +185,6 @@ class lia2pb_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result) { - SASSERT(g->is_well_sorted()); fail_if_proof_generation("lia2pb", g); m_produce_models = g->models_enabled(); m_produce_unsat_cores = g->unsat_core_enabled(); @@ -287,8 +286,6 @@ class lia2pb_tactic : public tactic { g->inc_depth(); g->add(gmc.get()); result.push_back(g.get()); - TRACE("lia2pb", g->display(tout);); - SASSERT(g->is_well_sorted()); } }; diff --git a/src/tactic/arith/nla2bv_tactic.cpp b/src/tactic/arith/nla2bv_tactic.cpp index dcf484dbc..49bde4e57 100644 --- a/src/tactic/arith/nla2bv_tactic.cpp +++ b/src/tactic/arith/nla2bv_tactic.cpp @@ -456,7 +456,6 @@ public: */ void operator()(goal_ref const & g, goal_ref_buffer & result) override { - SASSERT(g->is_well_sorted()); fail_if_proof_generation("nla2bv", g); fail_if_unsat_core_generation("nla2bv", g); result.reset(); @@ -467,7 +466,6 @@ public: proc(*(g.get()), mc); g->add(mc.get()); result.push_back(g.get()); - SASSERT(g->is_well_sorted()); } void cleanup() override { diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp index b1cb74f65..3cdf4ebf8 100644 --- a/src/tactic/arith/pb2bv_tactic.cpp +++ b/src/tactic/arith/pb2bv_tactic.cpp @@ -885,7 +885,6 @@ private: void operator()(goal_ref const & g, goal_ref_buffer & result) { TRACE("pb2bv", g->display(tout);); - SASSERT(g->is_well_sorted()); fail_if_proof_generation("pb2bv", g); m_produce_models = g->models_enabled(); m_produce_unsat_cores = g->unsat_core_enabled(); @@ -958,8 +957,6 @@ private: g->inc_depth(); result.push_back(g.get()); - TRACE("pb2bv", g->display(tout);); - SASSERT(g->is_well_sorted()); } void throw_tactic(expr* e) { diff --git a/src/tactic/arith/propagate_ineqs_tactic.cpp b/src/tactic/arith/propagate_ineqs_tactic.cpp index 8bde74c8c..a55a4334b 100644 --- a/src/tactic/arith/propagate_ineqs_tactic.cpp +++ b/src/tactic/arith/propagate_ineqs_tactic.cpp @@ -528,14 +528,13 @@ void propagate_ineqs_tactic::updt_params(params_ref const & p) { void propagate_ineqs_tactic::operator()(goal_ref const & g, goal_ref_buffer & result) { - SASSERT(g->is_well_sorted()); fail_if_proof_generation("propagate-ineqs", g); fail_if_unsat_core_generation("propagate-ineqs", g); result.reset(); goal_ref r; (*m_imp)(g.get(), r); result.push_back(r.get()); - SASSERT(r->is_well_sorted()); + SASSERT(r->is_well_formed()); } diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index 9cfd172fa..e180acd2c 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -910,7 +910,6 @@ public: void operator()(goal_ref const & g, goal_ref_buffer & result) override { try { - SASSERT(g->is_well_sorted()); tactic_report report("purify-arith", *g); TRACE("goal", g->display(tout);); bool produce_proofs = g->proofs_enabled(); @@ -924,8 +923,6 @@ public: g->add(mc.get()); g->inc_depth(); result.push_back(g.get()); - TRACE("goal", g->display(tout);); - SASSERT(g->is_well_sorted()); } catch (rewriter_exception & ex) { throw tactic_exception(ex.msg()); diff --git a/src/tactic/arith/recover_01_tactic.cpp b/src/tactic/arith/recover_01_tactic.cpp index 015ee1a86..a87ee2c92 100644 --- a/src/tactic/arith/recover_01_tactic.cpp +++ b/src/tactic/arith/recover_01_tactic.cpp @@ -293,7 +293,6 @@ class recover_01_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result) { - SASSERT(g->is_well_sorted()); fail_if_proof_generation("recover-01", g); fail_if_unsat_core_generation("recover-01", g); m_produce_models = g->models_enabled(); @@ -365,7 +364,7 @@ class recover_01_tactic : public tactic { } result.push_back(new_goal.get()); TRACE("recover_01", new_goal->display(tout);); - SASSERT(new_goal->is_well_sorted()); + SASSERT(new_goal->is_well_formed()); } ~imp() { diff --git a/src/tactic/bv/bv_bound_chk_tactic.cpp b/src/tactic/bv/bv_bound_chk_tactic.cpp index f71fcd5e4..3cb895c40 100644 --- a/src/tactic/bv/bv_bound_chk_tactic.cpp +++ b/src/tactic/bv/bv_bound_chk_tactic.cpp @@ -153,7 +153,6 @@ public: ast_manager& m() { return m_rw.m(); } void operator()(goal_ref const & g) { - SASSERT(g->is_well_sorted()); tactic_report report("bv-bound-chk", *g); ast_manager& m(g->m()); expr_ref new_curr(m); @@ -192,16 +191,12 @@ bv_bound_chk_tactic::~bv_bound_chk_tactic() { } void bv_bound_chk_tactic::operator()(goal_ref const & g, goal_ref_buffer & result) { - SASSERT(g->is_well_sorted()); fail_if_proof_generation("bv-bound-chk", g); fail_if_unsat_core_generation("bv-bound-chk", g); - TRACE("bv-bound-chk", g->display(tout << "before:"); tout << std::endl;); result.reset(); m_imp->operator()(g); g->inc_depth(); result.push_back(g.get()); - TRACE("bv-bound-chk", g->display(tout << "after:");); - SASSERT(g->is_well_sorted()); } tactic * bv_bound_chk_tactic::translate(ast_manager & m) { diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp index 68633ba85..0aff332a7 100644 --- a/src/tactic/bv/bv_size_reduction_tactic.cpp +++ b/src/tactic/bv/bv_size_reduction_tactic.cpp @@ -372,7 +372,6 @@ public: void bv_size_reduction_tactic::operator()(goal_ref const & g, goal_ref_buffer & result) { - SASSERT(g->is_well_sorted()); fail_if_proof_generation("bv-size-reduction", g); fail_if_unsat_core_generation("bv-size-reduction", g); TRACE("goal", g->display(tout);); @@ -382,7 +381,6 @@ void bv_size_reduction_tactic::operator()(goal_ref const & g, g->inc_depth(); g->add(mc.get()); result.push_back(g.get()); - SASSERT(g->is_well_sorted()); } } diff --git a/src/tactic/bv/bvarray2uf_tactic.cpp b/src/tactic/bv/bvarray2uf_tactic.cpp index 6bda3969b..b9fa9622a 100644 --- a/src/tactic/bv/bvarray2uf_tactic.cpp +++ b/src/tactic/bv/bvarray2uf_tactic.cpp @@ -55,12 +55,10 @@ class bvarray2uf_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result) { - SASSERT(g->is_well_sorted()); tactic_report report("bvarray2uf", *g); result.reset(); fail_if_unsat_core_generation("bvarray2uf", g); - TRACE("bvarray2uf", tout << "Before: " << std::endl; g->display(tout); ); m_produce_models = g->models_enabled(); model_converter_ref mc; @@ -93,8 +91,6 @@ class bvarray2uf_tactic : public tactic { g->inc_depth(); g->add(mc.get()); result.push_back(g.get()); - TRACE("bvarray2uf", tout << "After: " << std::endl; g->display(tout);); - SASSERT(g->is_well_sorted()); } void updt_params(params_ref const & p) { diff --git a/src/tactic/bv/dt2bv_tactic.cpp b/src/tactic/bv/dt2bv_tactic.cpp index 39d8cf5bb..5ea56fcbb 100644 --- a/src/tactic/bv/dt2bv_tactic.cpp +++ b/src/tactic/bv/dt2bv_tactic.cpp @@ -154,8 +154,6 @@ public: } g->inc_depth(); result.push_back(g.get()); - TRACE("dt2bv", g->display(tout);); - SASSERT(g->is_well_sorted()); } void cleanup() override { diff --git a/src/tactic/bv/elim_small_bv_tactic.cpp b/src/tactic/bv/elim_small_bv_tactic.cpp index 36bedcc5e..2f36f6bda 100644 --- a/src/tactic/bv/elim_small_bv_tactic.cpp +++ b/src/tactic/bv/elim_small_bv_tactic.cpp @@ -237,7 +237,6 @@ public: void operator()(goal_ref const & g, goal_ref_buffer & result) override { - SASSERT(g->is_well_sorted()); tactic_report report("elim-small-bv", *g); bool produce_proofs = g->proofs_enabled(); fail_if_proof_generation("elim-small-bv", g); @@ -261,8 +260,6 @@ public: report_tactic_progress(":elim-small-bv-num-eliminated", m_rw.m_cfg.m_num_eliminated); g->inc_depth(); result.push_back(g.get()); - TRACE("elim-small-bv", g->display(tout);); - SASSERT(g->is_well_sorted()); } void cleanup() override { diff --git a/src/tactic/bv/max_bv_sharing_tactic.cpp b/src/tactic/bv/max_bv_sharing_tactic.cpp index 71edd0a61..16e4b9679 100644 --- a/src/tactic/bv/max_bv_sharing_tactic.cpp +++ b/src/tactic/bv/max_bv_sharing_tactic.cpp @@ -236,7 +236,6 @@ class max_bv_sharing_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result) { - SASSERT(g->is_well_sorted()); tactic_report report("max-bv-sharing", *g); bool produce_proofs = g->proofs_enabled(); @@ -259,8 +258,6 @@ class max_bv_sharing_tactic : public tactic { m_rw.cfg().cleanup(); g->inc_depth(); result.push_back(g.get()); - TRACE("max_bv_sharing", g->display(tout);); - SASSERT(g->is_well_sorted()); } }; diff --git a/src/tactic/core/blast_term_ite_tactic.cpp b/src/tactic/core/blast_term_ite_tactic.cpp index 05924e32e..bdc146079 100644 --- a/src/tactic/core/blast_term_ite_tactic.cpp +++ b/src/tactic/core/blast_term_ite_tactic.cpp @@ -128,7 +128,6 @@ class blast_term_ite_tactic : public tactic { } void operator()(goal_ref const & g, goal_ref_buffer & result) { - SASSERT(g->is_well_sorted()); tactic_report report("blast-term-ite", *g); bool produce_proofs = g->proofs_enabled(); @@ -153,8 +152,6 @@ class blast_term_ite_tactic : public tactic { report_tactic_progress(":blast-term-ite-consts", m_rw.m_cfg.m_num_fresh + num_fresh); g->inc_depth(); result.push_back(g.get()); - TRACE("blast_term_ite", g->display(tout);); - SASSERT(g->is_well_sorted()); } }; diff --git a/src/tactic/core/cofactor_term_ite_tactic.cpp b/src/tactic/core/cofactor_term_ite_tactic.cpp index 4f52599cd..8260d59c7 100644 --- a/src/tactic/core/cofactor_term_ite_tactic.cpp +++ b/src/tactic/core/cofactor_term_ite_tactic.cpp @@ -55,15 +55,12 @@ public: void collect_param_descrs(param_descrs & r) override { m_elim_ite.collect_param_descrs(r); } void operator()(goal_ref const & g, goal_ref_buffer& result) override { - SASSERT(g->is_well_sorted()); fail_if_proof_generation("cofactor-term-ite", g); fail_if_unsat_core_generation("cofactor-term-ite", g); tactic_report report("cofactor-term-ite", *g); process(*(g.get())); g->inc_depth(); result.push_back(g.get()); - TRACE("cofactor-term-ite", g->display(tout);); - SASSERT(g->is_well_sorted()); } void cleanup() override { return m_elim_ite.cleanup(); } diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp index 4336ee1ac..7cad0d71e 100644 --- a/src/tactic/core/ctx_simplify_tactic.cpp +++ b/src/tactic/core/ctx_simplify_tactic.cpp @@ -569,7 +569,6 @@ struct ctx_simplify_tactic::imp { } void operator()(goal & g) { - SASSERT(g.is_well_sorted()); m_occs.reset(); m_occs(g); m_num_steps = 0; @@ -588,7 +587,6 @@ struct ctx_simplify_tactic::imp { process_goal(g); } IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "(ctx-simplify :num-steps " << m_num_steps << ")\n";); - SASSERT(g.is_well_sorted()); } }; diff --git a/src/tactic/core/der_tactic.cpp b/src/tactic/core/der_tactic.cpp index 8de00525e..f26202015 100644 --- a/src/tactic/core/der_tactic.cpp +++ b/src/tactic/core/der_tactic.cpp @@ -34,10 +34,8 @@ class der_tactic : public tactic { } void operator()(goal & g) { - SASSERT(g.is_well_sorted()); bool proofs_enabled = g.proofs_enabled(); tactic_report report("der", g); - TRACE("before_der", g.display(tout);); expr_ref new_curr(m()); proof_ref new_pr(m()); unsigned size = g.size(); @@ -53,8 +51,6 @@ class der_tactic : public tactic { g.update(idx, new_curr, new_pr, g.dep(idx)); } g.elim_redundancies(); - TRACE("after_der", g.display(tout);); - SASSERT(g.is_well_sorted()); } }; diff --git a/src/tactic/core/distribute_forall_tactic.cpp b/src/tactic/core/distribute_forall_tactic.cpp index 398af6103..aa1ef07c8 100644 --- a/src/tactic/core/distribute_forall_tactic.cpp +++ b/src/tactic/core/distribute_forall_tactic.cpp @@ -103,7 +103,6 @@ public: void operator()(goal_ref const & g, goal_ref_buffer & result) override { - SASSERT(g->is_well_sorted()); ast_manager & m = g->m(); bool produce_proofs = g->proofs_enabled(); rw r(m, produce_proofs); @@ -128,8 +127,6 @@ public: g->inc_depth(); result.push_back(g.get()); - TRACE("distribute-forall", g->display(tout);); - SASSERT(g->is_well_sorted()); m_rw = nullptr; } diff --git a/src/tactic/core/elim_term_ite_tactic.cpp b/src/tactic/core/elim_term_ite_tactic.cpp index a317b2ce0..c2d972b62 100644 --- a/src/tactic/core/elim_term_ite_tactic.cpp +++ b/src/tactic/core/elim_term_ite_tactic.cpp @@ -99,7 +99,6 @@ class elim_term_ite_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result) { - SASSERT(g->is_well_sorted()); tactic_report report("elim-term-ite", *g); bool produce_proofs = g->proofs_enabled(); m_rw.cfg().m_produce_models = g->models_enabled(); @@ -122,8 +121,6 @@ class elim_term_ite_tactic : public tactic { report_tactic_progress(":elim-term-ite-consts", m_rw.m_cfg.m_num_fresh); g->inc_depth(); result.push_back(g.get()); - TRACE("elim_term_ite", g->display(tout);); - SASSERT(g->is_well_sorted()); } }; diff --git a/src/tactic/core/injectivity_tactic.cpp b/src/tactic/core/injectivity_tactic.cpp index 69e5b4cee..0268179b5 100644 --- a/src/tactic/core/injectivity_tactic.cpp +++ b/src/tactic/core/injectivity_tactic.cpp @@ -145,7 +145,6 @@ class injectivity_tactic : public tactic { void operator()(goal_ref const & goal, goal_ref_buffer & result) { - SASSERT(goal->is_well_sorted()); tactic_report report("injectivity", *goal); fail_if_unsat_core_generation("injectivity", goal); // TODO: Support UNSAT cores fail_if_proof_generation("injectivity", goal); diff --git a/src/tactic/core/nnf_tactic.cpp b/src/tactic/core/nnf_tactic.cpp index f482181d2..3d64705d7 100644 --- a/src/tactic/core/nnf_tactic.cpp +++ b/src/tactic/core/nnf_tactic.cpp @@ -55,7 +55,6 @@ public: void operator()(goal_ref const & g, goal_ref_buffer & result) override { TRACE("nnf", tout << "params: " << m_params << "\n"; g->display(tout);); - SASSERT(g->is_well_sorted()); tactic_report report("nnf", *g); bool produce_proofs = g->proofs_enabled(); @@ -97,8 +96,6 @@ public: for (unsigned i = 0; i < num_extra_names; i++) fmc->hide(dnames.get_name_decl(i)); } - TRACE("nnf", g->display(tout);); - SASSERT(g->is_well_sorted()); } void cleanup() override {} diff --git a/src/tactic/core/occf_tactic.cpp b/src/tactic/core/occf_tactic.cpp index de8cb9375..9b90d27ef 100644 --- a/src/tactic/core/occf_tactic.cpp +++ b/src/tactic/core/occf_tactic.cpp @@ -127,7 +127,6 @@ class occf_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result) { - SASSERT(g->is_well_sorted()); fail_if_proof_generation("occf", g); bool produce_models = g->models_enabled(); @@ -181,8 +180,6 @@ class occf_tactic : public tactic { } g->inc_depth(); result.push_back(g.get()); - TRACE("occf", g->display(tout);); - SASSERT(g->is_well_sorted()); } }; diff --git a/src/tactic/core/pb_preprocess_tactic.cpp b/src/tactic/core/pb_preprocess_tactic.cpp index 1a583dac6..90c6cb217 100644 --- a/src/tactic/core/pb_preprocess_tactic.cpp +++ b/src/tactic/core/pb_preprocess_tactic.cpp @@ -110,8 +110,7 @@ public: void operator()( goal_ref const & g, goal_ref_buffer & result) override { - SASSERT(g->is_well_sorted()); - + tactic_report report("pb-preprocess", *g); if (g->proofs_enabled()) { throw tactic_exception("pb-preprocess does not support proofs"); } diff --git a/src/tactic/core/propagate_values_tactic.cpp b/src/tactic/core/propagate_values_tactic.cpp index 351b606e6..8a2e3dca9 100644 --- a/src/tactic/core/propagate_values_tactic.cpp +++ b/src/tactic/core/propagate_values_tactic.cpp @@ -123,7 +123,6 @@ class propagate_values_tactic : public tactic { } void run(goal_ref const & g, goal_ref_buffer & result) { - SASSERT(g->is_well_sorted()); tactic_report report("propagate-values", *g); m_goal = g.get(); @@ -189,7 +188,7 @@ class propagate_values_tactic : public tactic { m_goal->elim_redundancies(); m_goal->inc_depth(); result.push_back(m_goal); - SASSERT(m_goal->is_well_sorted()); + SASSERT(m_goal->is_well_formed()); TRACE("propagate_values", tout << "end\n"; m_goal->display(tout);); TRACE("propagate_values_core", m_goal->display_with_dependencies(tout);); m_goal = nullptr; diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp index a2ce8a801..390790c73 100644 --- a/src/tactic/core/reduce_args_tactic.cpp +++ b/src/tactic/core/reduce_args_tactic.cpp @@ -482,7 +482,6 @@ reduce_args_tactic::~reduce_args_tactic() { void reduce_args_tactic::operator()(goal_ref const & g, goal_ref_buffer & result) { - SASSERT(g->is_well_sorted()); fail_if_unsat_core_generation("reduce-args", g); result.reset(); if (!m_imp->m().proofs_enabled()) { @@ -490,7 +489,6 @@ void reduce_args_tactic::operator()(goal_ref const & g, } g->inc_depth(); result.push_back(g.get()); - SASSERT(g->is_well_sorted()); } void reduce_args_tactic::cleanup() { diff --git a/src/tactic/core/simplify_tactic.cpp b/src/tactic/core/simplify_tactic.cpp index 7e729714f..6ec2cbd38 100644 --- a/src/tactic/core/simplify_tactic.cpp +++ b/src/tactic/core/simplify_tactic.cpp @@ -43,7 +43,6 @@ struct simplify_tactic::imp { } void operator()(goal & g) { - SASSERT(g.is_well_sorted()); tactic_report report("simplifier", g); TRACE("before_simplifier", g.display(tout);); m_num_steps = 0; @@ -68,7 +67,6 @@ struct simplify_tactic::imp { g.elim_redundancies(); TRACE("after_simplifier", g.display(tout);); TRACE("after_simplifier_detail", g.display_with_dependencies(tout);); - SASSERT(g.is_well_sorted()); } unsigned get_num_steps() const { return m_num_steps; } diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp index f4d2f2b38..6a84bedfc 100644 --- a/src/tactic/core/solve_eqs_tactic.cpp +++ b/src/tactic/core/solve_eqs_tactic.cpp @@ -1008,7 +1008,6 @@ class solve_eqs_tactic : public tactic { } void operator()(goal_ref const & g, goal_ref_buffer & result) { - SASSERT(g->is_well_sorted()); model_converter_ref mc; tactic_report report("solve_eqs", *g); TRACE("goal", g->display(tout);); @@ -1047,8 +1046,6 @@ class solve_eqs_tactic : public tactic { g->inc_depth(); g->add(mc.get()); result.push_back(g.get()); - TRACE("goal", g->display(tout);); - SASSERT(g->is_well_sorted()); } }; diff --git a/src/tactic/core/split_clause_tactic.cpp b/src/tactic/core/split_clause_tactic.cpp index 138bc91ec..620a80e97 100644 --- a/src/tactic/core/split_clause_tactic.cpp +++ b/src/tactic/core/split_clause_tactic.cpp @@ -101,7 +101,6 @@ public: void operator()(goal_ref const & in, goal_ref_buffer & result) override { - SASSERT(in->is_well_sorted()); tactic_report report("split-clause", *in); TRACE("before_split_clause", in->display(tout);); ast_manager & m = in->m(); diff --git a/src/tactic/core/tseitin_cnf_tactic.cpp b/src/tactic/core/tseitin_cnf_tactic.cpp index bf4df2770..cc038aea3 100644 --- a/src/tactic/core/tseitin_cnf_tactic.cpp +++ b/src/tactic/core/tseitin_cnf_tactic.cpp @@ -830,7 +830,6 @@ class tseitin_cnf_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result) { - SASSERT(g->is_well_sorted()); tactic_report report("tseitin-cnf", *g); fail_if_proof_generation("tseitin-cnf", g); m_produce_models = g->models_enabled(); @@ -874,8 +873,6 @@ class tseitin_cnf_tactic : public tactic { g->add(m_mc.get()); g->inc_depth(); result.push_back(g.get()); - TRACE("tseitin_cnf", g->display(tout);); - SASSERT(g->is_well_sorted()); } }; diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp index e348c8859..e7804e05e 100644 --- a/src/tactic/fpa/fpa2bv_tactic.cpp +++ b/src/tactic/fpa/fpa2bv_tactic.cpp @@ -48,7 +48,6 @@ class fpa2bv_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result) { - SASSERT(g->is_well_sorted()); m_proofs_enabled = g->proofs_enabled(); m_produce_models = g->models_enabled(); m_produce_unsat_cores = g->unsat_core_enabled(); @@ -105,7 +104,6 @@ class fpa2bv_tactic : public tactic { for (unsigned i = 0; i < m_conv.m_extra_assertions.size(); i++) result.back()->assert_expr(m_conv.m_extra_assertions[i].get()); - SASSERT(g->is_well_sorted()); TRACE("fpa2bv", tout << "AFTER: " << std::endl; g->display(tout); if (g->mc()) g->mc()->display(tout); tout << std::endl; ); } diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp index 32725eba0..286f2864a 100644 --- a/src/tactic/goal.cpp +++ b/src/tactic/goal.cpp @@ -401,7 +401,6 @@ void goal::display_with_proofs(std::ostream& out) const { out << "\n |-"; if (pr(i)) { out << mk_ismt2_pp(pr(i), m(), 4); - SASSERT(m().get_fact(pr(i)) == form(i)); } out << "\n " << mk_ismt2_pp(form(i), m(), 2); } @@ -583,12 +582,17 @@ void goal::elim_redundancies() { shrink(j); } -bool goal::is_well_sorted() const { +bool goal::is_well_formed() const { unsigned sz = size(); for (unsigned i = 0; i < sz; i++) { expr * t = form(i); if (!::is_well_sorted(m(), t)) return false; +#if 0 + SASSERT(m().get_fact(pr(i)) == form(i)); + if (m().get_fact(pr(i)) != form(i)) + return false; +#endif } return true; } diff --git a/src/tactic/goal.h b/src/tactic/goal.h index ac376857e..b7bb16102 100644 --- a/src/tactic/goal.h +++ b/src/tactic/goal.h @@ -148,7 +148,7 @@ public: bool is_decided_sat() const; bool is_decided_unsat() const; bool is_decided() const; - bool is_well_sorted() const; + bool is_well_formed() const; dependency_converter* dc() { return m_dc.get(); } model_converter* mc() const { return m_mc.get(); } diff --git a/src/tactic/sine_filter.cpp b/src/tactic/sine_filter.cpp index 1612670a4..cca8a906c 100644 --- a/src/tactic/sine_filter.cpp +++ b/src/tactic/sine_filter.cpp @@ -60,7 +60,7 @@ public: g->updt_prec(goal::OVER); result.push_back(g.get()); TRACE("sine", result[0]->display(tout);); - SASSERT(g->is_well_sorted()); + SASSERT(g->is_well_formed()); } void cleanup() override { diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index 4a26a3716..12c6083a8 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -61,7 +61,6 @@ public: void operator()(goal_ref const & g, goal_ref_buffer & result) override { - SASSERT(g->is_well_sorted()); result.reset(); TRACE("sls", g->display(tout);); @@ -72,8 +71,6 @@ public: g->add(mc.get()); g->inc_depth(); result.push_back(g.get()); - TRACE("sls", g->display(tout);); - SASSERT(g->is_well_sorted()); } void cleanup() override { diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp index 898a7a232..6f2d844e1 100644 --- a/src/tactic/tactic.cpp +++ b/src/tactic/tactic.cpp @@ -35,11 +35,13 @@ struct tactic_report::imp { m_start_memory(static_cast(memory::get_allocation_size())/static_cast(1024*1024)) { m_watch.start(); TRACE("tactic", g.display_with_proofs(tout << id << "\n");); + SASSERT(g.is_well_formed()); } ~imp() { m_watch.stop(); double end_memory = static_cast(memory::get_allocation_size())/static_cast(1024*1024); + SASSERT(m_goal.is_well_formed()); TRACE("tactic", m_goal.display(tout);); IF_VERBOSE(0, verbose_stream() << "(" << m_id diff --git a/src/tactic/ufbv/macro_finder_tactic.cpp b/src/tactic/ufbv/macro_finder_tactic.cpp index 7b2cac6c2..2c0a529e6 100644 --- a/src/tactic/ufbv/macro_finder_tactic.cpp +++ b/src/tactic/ufbv/macro_finder_tactic.cpp @@ -39,7 +39,6 @@ class macro_finder_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result) { - SASSERT(g->is_well_sorted()); tactic_report report("macro-finder", *g); TRACE("macro-finder", g->display(tout);); @@ -76,8 +75,6 @@ class macro_finder_tactic : public tactic { g->add(evmc); g->inc_depth(); result.push_back(g.get()); - TRACE("macro-finder", g->display(tout);); - SASSERT(g->is_well_sorted()); } void updt_params(params_ref const & p) { diff --git a/src/tactic/ufbv/quasi_macros_tactic.cpp b/src/tactic/ufbv/quasi_macros_tactic.cpp index 39050ccc5..90c307d8c 100644 --- a/src/tactic/ufbv/quasi_macros_tactic.cpp +++ b/src/tactic/ufbv/quasi_macros_tactic.cpp @@ -37,7 +37,6 @@ class quasi_macros_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result) { - SASSERT(g->is_well_sorted()); tactic_report report("quasi-macros", *g); bool produce_proofs = g->proofs_enabled(); @@ -88,8 +87,6 @@ class quasi_macros_tactic : public tactic { g->add(evmc); g->inc_depth(); result.push_back(g.get()); - TRACE("quasi-macros", g->display(tout);); - SASSERT(g->is_well_sorted()); } void updt_params(params_ref const & p) { diff --git a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp index 9e41cee7c..9d197d8c9 100644 --- a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp +++ b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp @@ -43,7 +43,6 @@ public: } void operator()(goal_ref const & g, goal_ref_buffer & result) override { - SASSERT(g->is_well_sorted()); tactic_report report("ufbv-rewriter", *g); fail_if_unsat_core_generation("ufbv-rewriter", g); @@ -71,8 +70,6 @@ public: g->inc_depth(); result.push_back(g.get()); - TRACE("ufbv-rewriter", g->display(tout);); - SASSERT(g->is_well_sorted()); } void cleanup() override {}