From 53ca65a62ec2bc441784f7e2ebff1308a0d3c0ef Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 20 Mar 2023 18:55:40 +0100
Subject: [PATCH] fix unsound rewrite

---
 src/ast/rewriter/seq_rewriter.cpp | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index ea3e16f6e..6fd518cb0 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -5954,6 +5954,7 @@ bool seq_rewriter::reduce_non_overlap(expr_ref_vector& ls, expr_ref_vector& rs,
  */
 bool seq_rewriter::reduce_value_clash(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& eqs) {
     ptr_buffer<expr> es;
+
     if (ls.empty() || rs.empty())
         return true;
     es.append(ls.size(), ls.data());
@@ -5976,7 +5977,12 @@ bool seq_rewriter::reduce_value_clash(expr_ref_vector& ls, expr_ref_vector& rs,
         if (!is_unit_value(r))
             return true;
     }
-    return any_of(es, [&](expr* e) { return is_unit_value(e); });
+    if (es.empty())
+        return true;
+    for (expr* e : es)
+        if (!is_unit_value(e))
+            return true;
+    return false;
 }
 
 bool seq_rewriter::reduce_subsequence(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& eqs) {