mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-21 01:24:43 +00:00
Code Activity

Fix trail mechanism to capture state before modification

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-01-19 02:22:55 +00:00
parent 4be6d1894f
commit e3c1610335
1 changed files with 5 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/theory_finite_set_lattice_refutation.cpp
View file

@ -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)) {