mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
74621e0b7d
commit
5dc2b7172d
|
@ -701,7 +701,7 @@ namespace qe {
|
|||
}
|
||||
|
||||
void solve() {
|
||||
ptr_vector<term> worklist;
|
||||
ptr_vector<term> worklist;
|
||||
for (term * t : m_tg.m_terms) {
|
||||
// skip pure terms
|
||||
if (m_term2app.contains(t->get_id())) continue;
|
||||
|
@ -785,7 +785,8 @@ namespace qe {
|
|||
do {
|
||||
expr* member = mk_pure(*r);
|
||||
SASSERT(member);
|
||||
if (!members.contains(member) && (!is_projected(*r) || !is_solved_eq(rep, member))) {
|
||||
if (!members.contains(member) &&
|
||||
(!is_projected(*r) || !is_solved_eq(rep, member))) {
|
||||
res.push_back(m.mk_eq(rep, member));
|
||||
members.insert(member);
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue