A potential bug with CNF Examples while using dSharp #20
Description
Hi!
I recently encountered two issues while utilizing dSharp. I attempted to process two pairs CNF files using dSharp. I set the timeout of running the model counter to 600 seconds.
- For the first pair <origin1.cnf, new1.cnf>, the origin1.cnf file can be processed soon while the new1.cnf file cannot stop withing 600 seconds. The two files differ by only one clause (origin1.cnf is "42 -3 -4 82 51 0" while new1.cnf is "42 -3 -4 82 51 57 0") and produce completely opposite results. To assist the diagnosis, I conducted further tests: the critical clause "42 -3 -4 82 51 57 0" and the key variable "57" in new1.cnf, which seem to be causing the timeout.
- For the second pair < origin2.cnf, new2.cnf >, both attached files can be processed. But the new2.cnf file terminated abnormally and printed
bash: line 1: 627743 Killed ./dsharp /home/cstar/haiyan/model-counting/bench/order1/v100/cnf/new2.cnf.The printed content indicates that dSharp exhausted the system memory when processing new2.cnf and was killed by the system. Actually, the two files differ by only one literal ("-66") on the same clause (origin2.cnf is "14 -34 24 21 28 0" while new2.cnf is "14 -34 24 21 28 -66 0") and produce completely opposite difference.
I think dSharp may have potential bugs, and I hope this information can assist you to address the potential bugs. The two pairs example files are attached here for your reference.
Looking forward to your response. If you need any additional information or test data, please feel free to let me know. Thank you for your time and effort in developing this valuable tool.
Best regards,
Haiyan and Jifeng
CSTAR group