Closed
Description
A user reported potassco/clingo#425. While trying to come up with a minimal example that still triggers the bug. I stumbled over a program that triggers an assertion. I am not sure the two issues are related. Once the problem with the assertion is fixed, I can probably produce a much smaller program that triggers the problem in potassco/clingo#425 (if it then still exists).
Unfortunately, the assertion appears to be random. Seemingly unrelated changes to the program below make the assertion disappear. However, the program below reliably triggers it:
{q}.
a :- b.
c :- r.
b; r :- a.
a :- c.
l :- c.
n, k.
j, m.
t; v; w; x; y; z; aa; ab; ac; ad.
e; g.
f; h; i; j; l.
o; p.
a :- ae.
c :- ae.
a :- af.
c :- af.
ag; ah; ai; aj; ae; af.
➜ clingo bug-min.lp -q 0
clingo version 5.7.0 (161dbba)
Reading from bug-min.lp
Solving...
clingo: ./clasp/src/unfounded_check.cpp:607: void Clasp::DefaultUnfoundedCheck::createLoopFormula(): Assertion `solver_->isTrue(loopAtoms_.back()) && solver_->reason(loopAtoms_.back()) == this' failed.
zsh: IOT instruction clingo bug-min.lp -q 0
Or in ASPIF:
asp 1 0 0
1 0 6 1 2 3 4 5 6 0 0
1 0 1 7 0 1 6
1 0 1 8 0 1 6
1 0 1 7 0 1 5
1 0 1 8 0 1 5
1 0 2 9 10 0 0
1 0 5 11 12 13 14 15 0 0
1 0 2 16 17 0 0
1 0 10 18 19 20 21 22 23 24 25 26 27 0 0
1 0 2 14 28 0 0
1 0 2 29 30 0 0
1 0 1 8 0 1 7
1 0 2 31 32 0 1 8
1 0 1 8 0 1 31
1 0 1 7 0 1 32
1 0 1 15 0 1 7
1 1 1 33 0 0
0
➜ clasp bug.aspif -q 0
clasp version 3.3.9
Reading from bug.aspif
Solving...
clasp: ./clasp/src/unfounded_check.cpp:607: void Clasp::DefaultUnfoundedCheck::createLoopFormula(): Assertion `solver_->isTrue(loopAtoms_.back()) && solver_->reason(loopAtoms_.back()) == this' failed.
zsh: IOT instruction clasp bug.aspif -q 0
Metadata
Assignees
Labels
No labels