From e3c1610335e41605b4fdb753dacecd2db10ca5cd Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Mon, 19 Jan 2026 02:22:55 +0000
Subject: [PATCH] Fix trail mechanism to capture state before modification

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/smt/theory_finite_set_lattice_refutation.cpp | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/smt/theory_finite_set_lattice_refutation.cpp b/src/smt/theory_finite_set_lattice_refutation.cpp
index 068f41ce2..4e046d34e 100644
--- a/src/smt/theory_finite_set_lattice_refutation.cpp
+++ b/src/smt/theory_finite_set_lattice_refutation.cpp
@@ -25,7 +25,7 @@ namespace smt {
           non_link_justifications(MAX_VARS * MAX_VARS, {nullptr, nullptr}), largest_var(0),
           max_size(MAX_VARS), ctx(ctx), t_lattice_refutation(t_lattice) {
         // Initialize the vectors
-        link_dls.resize(MAX_VARS * MAX_VARS, 0);
+        link_dls.resize(MAX_VARS * MAX_VARS, static_cast<unsigned>(0));
         for (int i = 0; i < MAX_VARS; i++) {
             reachable[i].reset();
             non_links[i].reset();
@@ -53,16 +53,18 @@ namespace smt {
     }
 
     bool reachability_matrix::bitwise_or_rows(int source_dest, int source) {
-        // Save old state for potential rollback
+        // Save old state before modification
         uint_set old_reachable = reachable[source_dest];
         
+        // Push trail before modifying
+        ctx.push_trail(value_trail(reachable[source_dest]));
+        
         // Compute union: reachable[source_dest] |= reachable[source]
         reachable[source_dest] |= reachable[source];
         
         // Check if anything changed
         bool changes = !(old_reachable == reachable[source_dest]);
         if (changes) {
-            ctx.push_trail(value_trail(reachable[source_dest]));
             // Check for conflicts with newly added reachabilities
             for (unsigned dest : reachable[source_dest]) {
                 if (!old_reachable.contains(dest)) {