mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-18 18:36:41 +00:00
Code Activity

fix regression introduced when editing xor_gaussian

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-11-10 14:33:06 -08:00
parent 02f011c1e8
commit 07e2343c10
1 changed files with 4 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/sat/smt/xor_gaussian.cpp
View file

@ -1046,11 +1046,12 @@ void EGaussian::check_tracked_cols_only_one_set() {
<< " var: " << row_resp_for_var[found_row] + 1 << " var: " << row_resp_for_var[found_row] + 1
<< " and var: " << var + 1 << "\n";); << " and var: " << var + 1 << "\n";);
VERIFY(num_ones == 1); if (num_ones == 1) {
VERIFY(row_resp_for_var[found_row] == l_undef); VERIFY(row_resp_for_var[found_row] == l_undef);
row_resp_for_var[found_row] = var; row_resp_for_var[found_row] = var;
} }
} }
}
void EGaussian::check_invariants() { void EGaussian::check_invariants() {
if (!initialized) return; if (!initialized) return;