Closed jar-ben closed 4 years ago
Thanks, @jar-ben for analysis, I have added a fix. I ran buggy.cnf for half n hour and haven't seen the segfault.
@smsharma1, thanks for a quick fix! The file buggy.cnf is indeed quite hard to solve; unfortunately, I had no simpler benchmark that would cause the problem.
Ganak ends up with a segmentation fault when running on the attached .cnf file (executed as ./ganak buggy.cnf). I had to zip the .cnf file for upload so unzip it.
buggy.zip
The following is the report produced by valgrind: ==25159== Invalid read of size 8 ==25159== at 0x485561B: Instance::deleteConflictClauses() (instance.cpp:247) ==25159== by 0x485C2C7: Solver::resolveConflict() (solver.cpp:627) ==25159== by 0x485E6D7: Solver::countSAT() (solver.cpp:251) ==25159== by 0x4861210: Solver::solve(std::cxx11::basic_string<char, std::char_traits, std::allocator > const&) (solver.cpp:207)
==25159== by 0x10A426: main (main.cpp:168)
==25159== Address 0x0 is not stack'd, malloc'd or (recently) free'd
==25159==
==25159==
==25159== Process terminating with default action of signal 11 (SIGSEGV)
==25159== Access not within mapped region at address 0x0
==25159== at 0x485561B: Instance::deleteConflictClauses() (instance.cpp:247)
==25159== by 0x485C2C7: Solver::resolveConflict() (solver.cpp:627)
==25159== by 0x485E6D7: Solver::countSAT() (solver.cpp:251)
==25159== by 0x4861210: Solver::solve(std:: cxx11::basic_string<char, std::char_traits, std::allocator > const&) (solver.cpp:207)
==25159== by 0x10A426: main (main.cpp:168)
Based on my inspection of the code, the vector tmp_ratiosB (in function deleteConflictClauses (instance.cpp)) is empty when calling tmp_ratiosB[tmp_ratiosB.size()/2]. A possible fix is to check whether the vector is empty and if yes, then terminate the function (returning True). However, I do not know if this fix is sound (I do not know how exactly Ganak works).
Please, check the issue. Thanks, Jaroslav