From c1b355f34269581963d7003b709512d8fedc71c8 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 20 Oct 2022 17:48:17 -0700
Subject: [PATCH] #6364
throttle on upwards propagation of default was too restrictive
---
src/sat/smt/array_axioms.cpp | 4 ++++
src/sat/smt/array_solver.cpp | 5 ++---
2 files changed, 6 insertions(+), 3 deletions(-)
diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp
index 2c08b3e69..901344293 100644
--- a/src/sat/smt/array_axioms.cpp
+++ b/src/sat/smt/array_axioms.cpp
@@ -625,6 +625,10 @@ namespace array {
return change;
}
+ /**
+ * For every occurrence of as-array(f) and every occurrence of f(t)
+ * add equality select(as-array(f), t) = f(t)
+ */
bool solver::add_as_array_eqs(euf::enode* n) {
func_decl* f = nullptr;
bool change = false;
diff --git a/src/sat/smt/array_solver.cpp b/src/sat/smt/array_solver.cpp
index f66c2a183..2d3d13d3a 100644
--- a/src/sat/smt/array_solver.cpp
+++ b/src/sat/smt/array_solver.cpp
@@ -216,8 +216,7 @@ namespace array {
d.m_has_default = true;
for (euf::enode* lambda : d.m_lambdas)
push_axiom(default_axiom(lambda));
- if (should_prop_upward(d))
- propagate_parent_default(v);
+ propagate_parent_default(v);
}
void solver::propagate_select_axioms(var_data const& d, euf::enode* lambda) {
@@ -255,7 +254,7 @@ namespace array {
return;
ctx.push(reset_flag_trail(d.m_prop_upward));
d.m_prop_upward = true;
- if (should_prop_upward(d))
+ if (should_prop_upward(d))
propagate_parent_select_axioms(v);
set_prop_upward(d);
}