fix segfault on dDNNF output of unsat formula

crillab / d4

d4 Model Counter

GNU Lesser General Public License v3.0

14 stars 4 forks source link

fix segfault on dDNNF output of unsat formula #5

Closed symphorien closed 3 years ago

symphorien commented 3 years ago

to reproduce, on bug.cnf:

p cnf 1 2
1 0
-1 0

run

d4 -dDNNF bug.cnf

symphorien commented 3 years ago

cc @jm62300

jm62300 commented 3 years ago

Thx!

jm62300 commented 3 years ago

@symphorien I am working on a new version of d4 that will be available soon (actually it is ready but some parts remain unpublished and I would like to publish them before making a new release). If you have interesting benchmarks you cannot solve with the current version of d4 I can test on the new one. BTW, I am always interested in new problems using knowledge compilation and/or model counting, if you have such problems let me know we could discuss about improving d4 to tackle these problems.