From 942706e2716234283f8ad0dd66564a76e1f028a0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 31 Jan 2021 15:44:43 -0800
Subject: [PATCH] equality simplification

---
 src/ast/char_decl_plugin.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/ast/char_decl_plugin.cpp b/src/ast/char_decl_plugin.cpp
index fd9ec1f62..88e1778d1 100644
--- a/src/ast/char_decl_plugin.cpp
+++ b/src/ast/char_decl_plugin.cpp
@@ -114,6 +114,8 @@ expr* char_decl_plugin::get_some_value(sort* s) {
 app* char_decl_plugin::mk_le(expr* a, expr* b) {
     expr_ref _ch1(a, *m_manager), _ch2(b, *m_manager);
     unsigned v1 = 0, v2 = 0;
+    if (a == b)
+        return m_manager->mk_true();
     bool c1 = is_const_char(a, v1);
     bool c2 = is_const_char(b, v2);
     if (c1 && c2)