From 5cd1fe31fdd12954d7c8d92daa420cd1d1a4fe0d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 1 Jan 2022 20:37:26 -0800 Subject: [PATCH] propagate parent default not add parent default) Signed-off-by: Nikolaj Bjorner --- src/sat/smt/array_internalize.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/sat/smt/array_internalize.cpp b/src/sat/smt/array_internalize.cpp index b7b79ddbc..683cc5d07 100644 --- a/src/sat/smt/array_internalize.cpp +++ b/src/sat/smt/array_internalize.cpp @@ -163,8 +163,8 @@ namespace array { break; case OP_CONST_ARRAY: case OP_AS_ARRAY: - set_prop_upward(find(n)); - add_parent_default(find(n), n); + set_prop_upward(find(n)); + propagate_parent_default(find(n)); break; case OP_ARRAY_EXT: break;