From 03bb5a085facc26b4503d7dbc7c0efc289cab8a5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 15 Nov 2018 09:21:03 -0800 Subject: [PATCH] fix #1940 Signed-off-by: Nikolaj Bjorner --- src/ast/seq_decl_plugin.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 06f30cbdf..737213477 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -899,7 +899,7 @@ bool seq_decl_plugin::are_distinct(app* a, app* b) const { } if (is_app_of(a, m_family_id, OP_SEQ_UNIT) && is_app_of(b, m_family_id, OP_SEQ_UNIT)) { - return true; + return m_manager->are_distinct(a->get_arg(0), b->get_arg(0)); } if (is_app_of(a, m_family_id, OP_SEQ_EMPTY) && is_app_of(b, m_family_id, OP_SEQ_UNIT)) {