From bbb704e63c5708f0bb23ec558b2591301582c4be Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Thu, 2 Apr 2026 21:08:16 -0700
Subject: [PATCH] seq_axioms: eliminate redundant mk_literal call in add_clause
 (#9215)

* Initial plan

* 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>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
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]);