From 870ba21b84da627415de20fe31ad05d89eab2f2a 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:13 +0000
Subject: [PATCH] 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) {