invalid trace on small example

[jashug]

Running depqbf --dep-man=simple --trace=qrp --traditional-qcdcl test.qdimacs, with test.qdimacs containing:

p cnf 3 2
e 1 0
a 2 0
e 3 0
1 2 3 0
-1 -3 0

Produces trace:

p qrp 3 2
e 1 0
a 2 0
e 3 0
1 1 2 3 0 0
2 -1 -3 0 0
3 0 2 0
r SAT

(along with WARNING: tracing is not yet fully compatible with generalized axioms.) which qrpcheck -f test.qdimacs reports as an invalid proof.

This is seemingly because the proof involves an initial cube of -1 -3 0, which is invalid.

This issue could be what the warning is about, but I couldn't find a collection of options to produce a trace without the warning.

This is on depqbf version 6.03, compiled from source on Ubuntu.

[lonsing]

Thanks for pointing this out!

The following call disables techniques that are not yet supported in combination with trace generation:

./depqbf --dep-man=simple --trace=qrp --traditional-qcdcl --no-qbce-dynamic --no-dynamic-nenofex --no-trivial-falsity --no-trivial-truth ./test.qdimacs