mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

fix crash bugs in sat solver

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-11 11:27:10 -08:00
parent a6da207b65
commit d7f9a3b37d
1 changed files with 0 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/sat/sat_solver.cpp
View file

@ -566,9 +566,6 @@ namespace sat {
void solver::detach_nary_clause(clause & c) {
clause_offset cls_off = get_offset(c);
if (c.id() == 62805 && c.capacity() == 29) {
std::cout << "detach: " << c[0] << " " << c[1] << " size: " << c.size() << " cap: " << c.capacity() << " id: " << c.id() << "\n";
}
erase_clause_watch(get_wlist(~c[0]), cls_off);
erase_clause_watch(get_wlist(~c[1]), cls_off);
}