From 7735a40752859d84f743c4a776fe831740dd7b6b Mon Sep 17 00:00:00 2001 From: nikolajbjorner Date: Thu, 19 Feb 2015 07:01:55 -0800 Subject: [PATCH] fix bug in array simplification. Codeplex issue 173 Signed-off-by: nikolajbjorner --- .../simplifier/array_simplifier_plugin.cpp | 20 +++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) diff --git a/src/ast/simplifier/array_simplifier_plugin.cpp b/src/ast/simplifier/array_simplifier_plugin.cpp index c75766b25..221d2a209 100644 --- a/src/ast/simplifier/array_simplifier_plugin.cpp +++ b/src/ast/simplifier/array_simplifier_plugin.cpp @@ -327,18 +327,22 @@ void array_simplifier_plugin::get_stores(expr* n, unsigned& arity, expr*& m, ptr } lbool array_simplifier_plugin::eq_default(expr* def, unsigned arity, unsigned num_st, expr*const* const* st) { + bool all_diseq = m_manager.is_unique_value(def) && num_st > 0; + bool all_eq = true; for (unsigned i = 0; i < num_st; ++i) { - if (st[i][arity] == def) { - continue; - } - if (m_manager.is_unique_value(st[i][arity]) && m_manager.is_unique_value(def)) { - return l_false; - } - return l_undef; + all_eq &= (st[i][arity] == def); + all_diseq &= m_manager.is_unique_value(st[i][arity]) && (st[i][arity] != def); } - return l_true; + if (all_eq) { + return l_true; + } + if (all_diseq) { + return l_false; + } + return l_undef; } + bool array_simplifier_plugin::insert_table(expr* def, unsigned arity, unsigned num_st, expr*const* const* st, arg_table& table) { for (unsigned i = 0; i < num_st; ++i ) { for (unsigned j = 0; j < arity; ++j) {