mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Revert polarity in justifications

Browse source
This commit is contained in:
CEisenhofer 2022-12-07 15:54:58 +01:00
parent b5647f4d35
commit a32da52350
1 changed files with 0 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/sat/smt/xor_solver.cpp
View file

@ -237,7 +237,6 @@ namespace xr {
std::cout << "Justification from matrix " << j.get_matrix_idx() << " on row " << j.get_row_idx() << " (ID: " << ID << "):\n";
for (unsigned i = 0; i < cl->size(); i++) {
std::cout << (*cl)[i] << "(" << s().value((*cl)[i]) << ") ";
(*cl)[i].neg();
}
std::cout << std::endl;