From adec9372960c271d1e0b7f67706e8c926a333ead Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 27 Mar 2023 14:02:15 -0700 Subject: [PATCH] fix #6650 --- src/tactic/core/symmetry_reduce_tactic.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/tactic/core/symmetry_reduce_tactic.cpp b/src/tactic/core/symmetry_reduce_tactic.cpp index 9c308b60f7c..9ad12d504dc 100644 --- a/src/tactic/core/symmetry_reduce_tactic.cpp +++ b/src/tactic/core/symmetry_reduce_tactic.cpp @@ -146,9 +146,10 @@ class symmetry_reduce_tactic::imp { app* c = select_const(consts, cts); if (!c) break; cts.push_back(c); - expr_ref mem(mk_member(t, cts), m); + expr_ref mem = mk_member(t, cts); g.assert_expr(mem); num_sym_break_preds++; + TRACE("symmetry_reduce", tout << "member predicate: " << mem << "\n";); fml = m.mk_and(fml.get(), mem); @@ -592,7 +593,7 @@ class symmetry_reduce_tactic::imp { return (j == A.size())? nullptr:A[j]; } - expr* mk_member(app* t, term_set const& C) { + expr_ref mk_member(app* t, term_set const& C) { expr_ref_vector eqs(m); for (expr* e : C) eqs.push_back(m.mk_eq(t, e));