Integer overflow

[hughescr]

This can't be good:

plingeling.c:456:17: warning: signed shift result (0x300000000) requires 35 bits to represent, but 'int' only has 32 bits [-Wshift-overflow] res = MAXGB << 30;;

[xiw]

STACK performs its analysis on the IR emitted by the clang frontend. In this case clang already folds the shift operation to a constant before emitting the IR, so there's nothing STACK can do about it. You could change clang not to perform the constant folding, or find another frontend.

[xiw]

Another possible workaround is to write a clang plugin to disable constant folding, for example, by converting the shift operation into a function call.

[hughescr]

Modifying plingeling.c inside lingeling-al6-080d45d-120922.tar.gz to have this at line 20 removes the warning/error:

define MAXGB 12LL

[msoos]

Yeah, that's probably a memory limit. Lingeling has its own memory manager for at least the clause database. I guess that could be it. However, the offsets could be stuffed (with extra data), so beware that increasing that value might break things. I suggest stack to simplify the problem a bit before passing it to lingeling: anything that eats so much memory that lingeling has problems with will probably be slow.

[hughescr]

And again as with the other bug, whether lingeling fixes it upstream or not, you should get the warning out in your local copy.

[xiw]

Oops I misread your report. This is an issue in the Lingeling solver, which I reported upstream a while ago. I don't have the expertise to fix it. I'll check its latest code. Thanks.

[xiw]

Fixed in 9fbdeb8e40be9e9cde9c9c1f54df17430ff0748b. STACK doesn't need this file. Thanks.