{"push_id":588615916,"size":2,"distinct_size":2,"ref":"refs/heads/ticket/SI-9181","head":"d904f5dcdb8d8376cdacf93bdd103afc6a222719","before":"aba16266c17528e089a283e775392e97e7c84710","commits":[{"sha":"6a4f00418ea272545bb074dcd8fe376218d02244","author":{"email":"af9d50c5890ef203d7cd74146c0743c9e4caadf5@gmail.com","name":"Gerard Basler"},"message":"Add a check to ensure that if the formulas originating from the exhaustivity /\nreachability analysis are too big to be solved in reasonable time, then we skip\nthe analysis. I also cleaned up warnings.\n\nWhy did `t9181.scala` work fine with 2.11.4, but is now running out of memory?\n\nIn order to ensure that the scrutinee is associated only with one of the 400\nderived classes we add 400*400 / 2 ~ 80k clauses to ensure mutual exclusivity.\n\nIn 2.11.4 the translation into CNF used to fail, since it would blow up already\nat this point in memory. This has been fixed in 2.11.5, but now the DPLL solver\nis the bottleneck.\n\nThere's a check in the search for all models (exhaustivity) that it would avoid\na blow up, but in the search for a model (reachability), such a check is\nmissing.","distinct":true,"url":"https://api.github.com/repos/gbasler/scala/commits/6a4f00418ea272545bb074dcd8fe376218d02244"},{"sha":"d904f5dcdb8d8376cdacf93bdd103afc6a222719","author":{"email":"af9d50c5890ef203d7cd74146c0743c9e4caadf5@gmail.com","name":"Gerard Basler"},"message":"Bring back improvements from `SI-6942` that were lost during the switch to\nTseitin's transformation, e.g., use\n\n`CNF(P1 /\\ ... /\\ PN) == CNF(P1) ++ CNF(...) ++ CNF(PN)`\n\nin order to simplify the resultung formula.","distinct":true,"url":"https://api.github.com/repos/gbasler/scala/commits/d904f5dcdb8d8376cdacf93bdd103afc6a222719"}]}