From 25d54ebb403323de327d1394292bf110af4f348f Mon Sep 17 00:00:00 2001
From: Margus Veanes <veanes@users.noreply.github.com>
Date: Sun, 19 Dec 2021 14:07:53 -0800
Subject: [PATCH] fixing regression of issue 1224 (#5723)

---
 src/ast/rewriter/seq_rewriter.cpp | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index aef5eeacd..58918567e 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -4956,6 +4956,7 @@ 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;
     if (u().is_char(elem)) {
         unsigned ch = 0, ch2 = 0;
         svector<std::pair<unsigned, unsigned>> ranges, ranges1;
@@ -4980,7 +4981,6 @@ void seq_rewriter::elim_condition(expr* elem, expr_ref& cond) {
                 ranges.append(ranges1);
             }
         };
-        bool all_ranges = true;
         bool negated = false;
         for (expr* e : conds) {
             if (u().is_char_const_range(elem, e, ch, ch2, negated)) {
@@ -5030,7 +5030,6 @@ void seq_rewriter::elim_condition(expr* elem, expr_ref& cond) {
                 cond = m().mk_true();
                 return;
             }
-            // removes all the trivially true conditions from conds
             conds.set(conds_range);
         }
     }
@@ -5054,6 +5053,13 @@ void seq_rewriter::elim_condition(expr* elem, expr_ref& cond) {
             cond = m().mk_and(m().mk_eq(elem, solution), cond);
         }
     }    
+    else if (all_ranges) {
+        if (conds.empty())
+            // all ranges were removed as trivially true
+            cond = m().mk_true();
+        else
+            cond = m().mk_and(conds_range);
+    }
 }