From d89532a33d90aae62fae0e9695b618701eca0b27 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Thu, 5 Mar 2026 17:58:32 +0000
Subject: [PATCH 1/2] Initial plan


From 822f19819cd2c05ee9b7794dd823f3366602636b Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Thu, 5 Mar 2026 17:59:50 +0000
Subject: [PATCH 2/2] Remove unreachable return false in match_ubv2s1

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/ast/rewriter/seq_eq_solver.cpp | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/ast/rewriter/seq_eq_solver.cpp b/src/ast/rewriter/seq_eq_solver.cpp
index c6778c45e..e1ffae743 100644
--- a/src/ast/rewriter/seq_eq_solver.cpp
+++ b/src/ast/rewriter/seq_eq_solver.cpp
@@ -226,7 +226,6 @@ namespace seq {
         return
             e.ls.size() == 1 && e.rs.size() == 1 &&
             seq.str.is_ubv2s(e.ls[0], a) && seq.str.is_ubv2s(e.rs[0], b);
-        return false;
     }
 
     bool eq_solver::reduce_ubv2s1(eqr const& e, eq_ptr& r) {