From 40b33ab35378f3f3473b06cb4eb6c3ac176d981b Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Tue, 10 Mar 2026 17:10:36 +0000
Subject: [PATCH] Address code review: simplify constructor, add UNREACHABLE()

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/smt/seq/seq_nielsen.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 9ab617ea2..ea75ecc17 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -620,7 +620,7 @@ namespace seq {
 
     nielsen_graph::nielsen_graph(euf::sgraph& sg, simple_solver* solver):
         m_sg(sg),
-        m_solver(solver ? solver : nullptr) {
+        m_solver(solver) {
         if (!m_solver) {
             m_owned_solver = alloc(lp_simple_solver, sg.get_manager());
             m_solver = m_owned_solver.get();
@@ -2742,6 +2742,7 @@ namespace seq {
         case int_constraint_kind::ge:
             return expr_ref(arith.mk_ge(ic.m_lhs, ic.m_rhs), m);
         }
+        UNREACHABLE();
         return expr_ref(m.mk_true(), m);
     }