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

fix #6650

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-03-27 14:02:15 -07:00
parent f366772f0c
commit adec937296
1 changed files with 3 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/tactic/core/symmetry_reduce_tactic.cpp
View file

@ -146,9 +146,10 @@ public:
app* c = select_const(consts, cts); app* c = select_const(consts, cts);
if (!c) break; if (!c) break;
cts.push_back(c); cts.push_back(c);
expr_ref mem(mk_member(t, cts), m); expr_ref mem = mk_member(t, cts);
g.assert_expr(mem); g.assert_expr(mem);
num_sym_break_preds++; num_sym_break_preds++;
TRACE("symmetry_reduce", tout << "member predicate: " << mem << "\n";); TRACE("symmetry_reduce", tout << "member predicate: " << mem << "\n";);
fml = m.mk_and(fml.get(), mem); fml = m.mk_and(fml.get(), mem);
@ -592,7 +593,7 @@ private:
return (j == A.size())? nullptr:A[j]; 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); expr_ref_vector eqs(m);
for (expr* e : C) for (expr* e : C)
eqs.push_back(m.mk_eq(t, e)); eqs.push_back(m.mk_eq(t, e));