Very brittle propagator-check performance

I came across strange performance behavior with the propagator with the option check_only=True.

In a simple problem with a domain of size 16,17, or 1000, for one variable, depending on whether an external atom declaration is present, the performance changes dramatically. The external atom is not referenced anywhere. The discrepancy does not depend on grounding.

The presence of the external atom changes slightly the ordering of the literals clasp uses internally but the magnitude of the impact surprises me (I'd have expected a *2 factor at most).

@kstrauch94 and @MaxOstrowski , any clue what could be happening?

clingo tests/investigate/slowdown.16.next.lp -q | grep Unsat
Time         : 0.082s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)

clingo tests/investigate/slowdown.16.yext.lp -q | grep Unsat
Time         : 0.090s (Solving: 0.01s 1st Model: 0.01s Unsat: 0.00s)

clingo tests/investigate/slowdown.17.next.lp -q | grep Unsat
Time         : 9.994s (Solving: 9.92s 1st Model: 9.91s Unsat: 0.00s)

clingo tests/investigate/slowdown.17.yext.lp -q | grep Unsat
Time         : 47.599s (Solving: 47.52s 1st Model: 47.52s Unsat: 0.00s)

clingo tests/investigate/slowdown.1000.next.lp -q | grep Unsat
Time         : 1.914s (Solving: 1.64s 1st Model: 1.04s Unsat: 0.00s)

clingo tests/investigate/slowdown.1000.next.lp -q | grep Unsat
[interrupted after 300s]

Instance:

#const int_domain_size = 16. % or 17 or 1000
#external neverUsed. % or commented out

variable_declare(x,fromFacts).
variable_domain(x,val(int,1..int_domain_size)).
variable_define(y,operation(add,(variable(x),(val(int,1),())))).
ensure(max_domain_value,operation(eq,(variable(y),(val(int,int_domain_size+1),())))).

Tested on commit afee4769b8839efa949daf86c6acaa6fd5495eb2

Start by reproducing the commands against tests/investigate/slowdown.16.next.lp, slowdown.16.yext.lp, slowdown.17.next.lp, and slowdown.17.yext.lp, including the 1000-sized instance. Compare behavior with and without the unused #external declaration, then trace the propagator check and clasp literal-ordering effects; done means identifying and documenting the source of the performance discrepancy.