From be38b256c88052d4b62f308880631a6480359019 Mon Sep 17 00:00:00 2001
From: Margus Veanes <veanes@users.noreply.github.com>
Date: Sun, 19 Dec 2021 17:46:42 -0800
Subject: [PATCH] fixed bug in is_char_const_range (#5724)

---
 src/ast/rewriter/seq_rewriter.cpp | 7 +++++--
 src/ast/seq_decl_plugin.cpp       | 8 ++++----
 2 files changed, 9 insertions(+), 6 deletions(-)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 58918567e..aeda76da5 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -4956,8 +4956,9 @@ void seq_rewriter::elim_condition(expr* elem, expr_ref& cond) {
     expr_ref_vector conds_range(m());
     flatten_and(cond, conds);
     expr* lhs = nullptr, *rhs = nullptr, *e1 = nullptr; 
-    bool all_ranges = true;
+    bool all_ranges = false;
     if (u().is_char(elem)) {
+        all_ranges = true;
         unsigned ch = 0, ch2 = 0;
         svector<std::pair<unsigned, unsigned>> ranges, ranges1;
         ranges.push_back(std::make_pair(0, u().max_char()));
@@ -5057,8 +5058,10 @@ void seq_rewriter::elim_condition(expr* elem, expr_ref& cond) {
         if (conds.empty())
             // all ranges were removed as trivially true
             cond = m().mk_true();
+        else if (conds.size() == 1)
+            cond = conds.get(0);
         else
-            cond = m().mk_and(conds_range);
+            cond = m().mk_and(conds);
     }
 }
 
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 98a77c6b8..091f77f5c 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -832,7 +832,7 @@ app* seq_util::mk_lt(expr* ch1, expr* ch2) const {
 }
 
 bool seq_util::is_char_const_range(expr const* x, expr* e, unsigned& l, unsigned& u, bool& negated) const {
-    expr* a, * b, * e1, * e2, * lb, * ub;
+    expr* a, * b, * e0, * e1, * e2, * lb, * ub;
     e1 = e;
     negated = (m.is_not(e, e1)) ? true : false;
     if (m.is_eq(e1, a, b) && (a == x && is_const_char(b, l))) {
@@ -849,7 +849,7 @@ bool seq_util::is_char_const_range(expr const* x, expr* e, unsigned& l, unsigned
         u = max_char();
         return true;
     }
-    if (m.is_and(e1, e1, e2) && is_char_le(e1, lb, a) && a == x && is_const_char(lb, l) &&
+    if (m.is_and(e1, e0, e2) && is_char_le(e0, lb, a) && a == x && is_const_char(lb, l) &&
         is_char_le(e2, b, ub) && b == x && is_const_char(ub, u))
         // (l <= x) & (x <= u)
         return true;
@@ -857,8 +857,8 @@ bool seq_util::is_char_const_range(expr const* x, expr* e, unsigned& l, unsigned
         u = l;
         return true;
     }
-    if (m.is_and(e1, e2, e1) && is_char_le(e1, lb, a) && a == x && is_const_char(lb, l) &&
-        is_char_le(e2, b, ub) && b == x && is_const_char(ub, u))
+    if (m.is_and(e1, e0, e2) && is_char_le(e0, a, ub) && a == x && is_const_char(ub, u) &&
+        is_char_le(e2, lb, b) && b == x && is_const_char(lb, l))
         // (x <= u) & (l <= x)
         return true;
     return false;