Embedded CVC4 for Android is broken: even a simple test case can cause it to go in the woods and never terminate. A stack trace show it is stuck in quantifier instantiation, trying to exhaustively enumerate all integers.
Because quantifiers should be disabled in our problems, I suspect memory corruption (possibly in option parsing) or a miscompilation. It could also be a lack of good a randomness source, or some other weird Android specific issue.
For now, I adopted the nuclear option (throwing the problem at a server, running a known good version of CVC4), but this is not long-term viable so we should revisit this.
gcampax
commented
5 years ago
Embedded CVC4 for Android is broken: even a simple test case can cause it to go in the woods and never terminate. A stack trace show it is stuck in quantifier instantiation, trying to exhaustively enumerate all integers. Because quantifiers should be disabled in our problems, I suspect memory corruption (possibly in option parsing) or a miscompilation. It could also be a lack of good a randomness source, or some other weird Android specific issue.
For now, I adopted the nuclear option (throwing the problem at a server, running a known good version of CVC4), but this is not long-term viable so we should revisit this.