Open DerZc opened 1 year ago
I find if I remove the subsumption of vdvr
, the program can execute correctly with -t none
.
Hi,
I reduce the program, hope this can help you fix this bug.
.decl yemn(A:unsigned)
.decl vdvr(A:unsigned, B:unsigned, C:unsigned)
yemn(0).
vdvr(B, B, B) :- yemn(B).
vdvr(B, B, B1) <= vdvr(B, B, B2) :- B1=B2.
.output vdvr
Subsumptive clauses were not implemented in the provenance system. That is missing! Great find.
Either we need to report an issue or implement subsumptive clauses in the provenance system.
I am very glad that this finding can help you and hope that other findings can be useful to you as well.
Hi,
This program assertion failure on provenance with
-t none
:The command is
souffle -w -t none example.dl
. Get the result:It run correctly without
-t none
. I don't know whether it is a feature related to #2316