From 378097b5ffed83d8d0c014fdccd5470161e721dd Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Fri, 3 Apr 2026 01:40:49 +0000
Subject: [PATCH] fix: use already-computed literal in seq_axioms::add_clause

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/0ab6afce-13a9-4e77-87b4-e416bc06f413

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

diff --git a/src/smt/seq_axioms.cpp b/src/smt/seq_axioms.cpp
index bd4d8dec2..ad8afcf42 100644
--- a/src/smt/seq_axioms.cpp
+++ b/src/smt/seq_axioms.cpp
@@ -97,7 +97,7 @@ void seq_axioms::add_clause(expr_ref_vector const& clause) {
         if (lit == true_literal)
             return;
         if (lit != false_literal)
-            lits[idx++] = mk_literal(e);
+            lits[idx++] = lit;
         SASSERT(idx <= 5);
     }
     add_axiom(lits[0], lits[1], lits[2], lits[3], lits[4]);