lonsing
Inconsistent behaviour of `--qdo` on input with no clauses
Consider the following input: a formula with 4 variables and no clauses.
p cnf 4 0
e 1 2 3 4 0
Running depqbf on it returns SAT as expected. However, running depqbf --no-dynamic-nenofex --qdo on the same input segfaults:
s cnf 1 4 0
Segmentation fault (core dumped)
It would be desirable to return any model (ideal case) or some error message stating that inputs with no clauses are not accepted (in which case depqbf should be made to reject those inputs as well, for the sake of consistency).
(By the way, thank you for the great tool!)
After a bit more testing, I realize that the issue does not specifically stem from the absence of clauses the following input triggers the same inconsistent behaviour based on whether --qdo is enabled or not.
p cnf 4 1
e 1 2 3 4 0
4 -4 0