From f8e2fa03379d752fc400376f312a5d8115e173fa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 29 May 2015 11:11:13 -0700 Subject: [PATCH] fixes issue #93 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_array_full.cpp | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp index dd74f2871..f2d1527c0 100644 --- a/src/smt/theory_array_full.cpp +++ b/src/smt/theory_array_full.cpp @@ -775,17 +775,19 @@ namespace smt { bool theory_array_full::try_assign_eq(expr* v1, expr* v2) { + TRACE("array", + tout << mk_bounded_pp(v1, get_manager()) << "\n==\n" + << mk_bounded_pp(v2, get_manager()) << "\n";); context& ctx = get_context(); if (m_eqs.contains(v1, v2)) { return false; } - m_eqs.insert(v1, v2, true); - TRACE("array", - tout << mk_bounded_pp(v1, get_manager()) << "\n==\n" - << mk_bounded_pp(v2, get_manager()) << "\n";); - literal eq(mk_eq(v1, v2, true)); - m_eqsv.push_back(eq); - return true; + else { + m_eqs.insert(v1, v2, true); + literal eq(mk_eq(v1, v2, true)); + m_eqsv.push_back(eq); + return true; + } } void theory_array_full::pop_scope_eh(unsigned num_scopes) {