Empty statement with continues

[hughescr]

These are probably all incorrect code. There should be no semi-colon before the "continue", unless the "continue" is supposed to apply to the outer scope.

lglib.c:9646:39: warning: while loop has empty body [-Wempty-body] if (other >= NOTALIT) { while (_q++) ; continue; } ^ lglib.c:9646:39: note: put the semicolon on a separate line to silence this warning lglib.c:10067:51: warning: for loop has empty body [-Wempty-body] if (_c == REMOVED) { for (p = c + 1; _p; p++) ; continue; } ^ lglib.c:10067:51: note: put the semicolon on a separate line to silence this warning lglib.c:10087:53: warning: for loop has empty body [-Wempty-body] if (_d == REMOVED) { for (q = d + 1; _q; q++) ; continue; } ^ lglib.c:10087:53: note: put the semicolon on a separate line to silence this warning lglib.c:10309:51: warning: for loop has empty body [-Wempty-body] if (_c == REMOVED) { for (p = c + 1; _p; p++) ; continue; } ^ lglib.c:10309:51: note: put the semicolon on a separate line to silence this warning lglib.c:10325:53: warning: for loop has empty body [-Wempty-body] if (_d == REMOVED) { for (q = d + 1; _q; q++) ; continue; } ^ lglib.c:10325:53: note: put the semicolon on a separate line to silence this warning lglib.c:10389:51: warning: for loop has empty body [-Wempty-body] if (_c == REMOVED) { for (p = c + 1; _p; p++) ; continue; } ^ lglib.c:10389:51: note: put the semicolon on a separate line to silence this warning lglib.c:10403:51: warning: for loop has empty body [-Wempty-body] if (_c == REMOVED) { for (p = c + 1; _p; p++) ; continue; } ^ lglib.c:10403:51: note: put the semicolon on a separate line to silence this warning lglib.c:10419:53: warning: for loop has empty body [-Wempty-body] if (_d == REMOVED) { for (q = d + 1; *q; q++) ; continue; }

[hughescr]

to be clear, this code should probably be re-written as either: if (other >= NOTALIT) { while (q++) continue; continue; } or if (other >= NOTALIT) { while (q++) continue; }

depending on which semantics are wanted -- continuing the outer loop, or the inner one, respectively

[msoos]

This is ligeling code. You have to talk to Armin Biere about this, I think. He doesn't have an online repo or bugtracker, though, so email is your best choice I think. He is kind and will probably reply promptly.

Do note that the new lingelings are not free (as in MIT/GPL/LGPL/Apache/etc.) anymore, so you may want to think about whether helping a commercial system is in your best interest.

[hughescr]

Whether upstream fixes it or not, you should fix it in your copy :) But yeah, my inclination to help out a non-open project (for free, anyway) is limited.

[xiw]

@hughescr We don't have the expertise the fix the Lingeling solver. You should report this upstream, or choose another SAT solver, such as PicoSAT and MiniSAT, which also work with Boolector.

@msoos Thanks for explaining this!