From 6f2fde87d1a58469cbc7f5a357aa9cab7cc7c3b5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 24 Sep 2022 14:40:30 -0700 Subject: [PATCH] move has-default up before merge of parents Signed-off-by: Nikolaj Bjorner --- src/sat/smt/array_solver.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/sat/smt/array_solver.cpp b/src/sat/smt/array_solver.cpp index 1c4b95abe..f66c2a183 100644 --- a/src/sat/smt/array_solver.cpp +++ b/src/sat/smt/array_solver.cpp @@ -164,6 +164,10 @@ namespace array { auto& d2 = get_var_data(v2); if (d2.m_prop_upward && !d1.m_prop_upward) set_prop_upward(v1); + if (d1.m_has_default && !d2.m_has_default) + add_parent_default(v2); + if (!d1.m_has_default && d2.m_has_default) + add_parent_default(v1); for (euf::enode* lambda : d2.m_lambdas) add_lambda(v1, lambda); for (euf::enode* lambda : d2.m_parent_lambdas) @@ -172,10 +176,6 @@ namespace array { add_parent_select(v1, select); if (is_lambda(e1) || is_lambda(e2)) push_axiom(congruence_axiom(n1, n2)); - if (d1.m_has_default && !d2.m_has_default) - add_parent_default(v2); - if (!d1.m_has_default && d2.m_has_default) - add_parent_default(v1); } void solver::add_parent_select(theory_var v_child, euf::enode* select) {