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

chore(datatype): small improvements

Browse source
This commit is contained in:
Simon Cruanes 2018-04-03 12:12:09 -05:00
parent fa10e510bb
commit e535cad480
2 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_datatype.cpp
View file

@ -393,7 +393,7 @@ namespace smt {
for (int v = 0; v < num_vars; v++) { for (int v = 0; v < num_vars; v++) {
if (v == static_cast<int>(m_find.find(v))) { if (v == static_cast<int>(m_find.find(v))) {
enode * node = get_enode(v); enode * node = get_enode(v);
if (occurs_check(node)) { if (!oc_cycle_free(node) && occurs_check(node)) {
// conflict was detected... // conflict was detected...
// return... // return...
return FC_CONTINUE; return FC_CONTINUE;

3
src/smt/theory_datatype.h
View file

@ -104,8 +104,8 @@ namespace smt {
theory_datatype * th; theory_datatype * th;
public: public:
final_check_st(theory_datatype * th) : th(th) { final_check_st(theory_datatype * th) : th(th) {
th->m_to_unmark2.reset();
th->m_to_unmark.reset(); th->m_to_unmark.reset();
th->m_to_unmark2.reset();
th->m_used_eqs.reset(); th->m_used_eqs.reset();
th->m_stack.reset(); th->m_stack.reset();
th->m_parent.reset(); th->m_parent.reset();
@ -115,6 +115,7 @@ namespace smt {
unmark_enodes2(th->m_to_unmark2.size(), th->m_to_unmark2.c_ptr()); unmark_enodes2(th->m_to_unmark2.size(), th->m_to_unmark2.c_ptr());
th->m_to_unmark.reset(); th->m_to_unmark.reset();
th->m_to_unmark2.reset(); th->m_to_unmark2.reset();
th->m_used_eqs.reset();
th->m_stack.reset(); th->m_stack.reset();
th->m_parent.reset(); th->m_parent.reset();
} }