{"push_id":796039449,"size":53,"distinct_size":53,"ref":"refs/heads/trunk","head":"f83b6d709a5c9198407fb0e699b5ffabf47d08b9","before":"a89cbe0a6bc8e74ae88a14221d76b80c5ea1229a","commits":[{"sha":"82c4e7d860c0ae6e9f75526a381b203c4f62f8d9","author":{"email":"fdf48669bf30a1b7cf144e2d79bb8eed9c068d7d@4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c","name":"lukasczyk"},"message":"Add support for array formulas in SMTInterpol. This is not fully working yet, do not use!\n\ngit-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@17764 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c","distinct":true,"url":"https://api.github.com/repos/petr-muller/cpachecker/commits/82c4e7d860c0ae6e9f75526a381b203c4f62f8d9"},{"sha":"e01a1d2fa9735063a352f3b7f97d2c998daf20f9","author":{"email":"fdf48669bf30a1b7cf144e2d79bb8eed9c068d7d@4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c","name":"lukasczyk"},"message":"Fixing test fail until SMTInterpol's logic was changed to an array supporting.\n\ngit-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@17765 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c","distinct":true,"url":"https://api.github.com/repos/petr-muller/cpachecker/commits/e01a1d2fa9735063a352f3b7f97d2c998daf20f9"},{"sha":"263f3ab09126551e48715e4c1d85ced295603a6d","author":{"email":"fafbb143bc98b3398fb52cc5dc97b0add41e1a09@gmail.com","name":"George Karpenkov"},"message":"LPI: handle the case when multiple siblings are present properly.\n\ngit-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@17766 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c","distinct":true,"url":"https://api.github.com/repos/petr-muller/cpachecker/commits/263f3ab09126551e48715e4c1d85ced295603a6d"},{"sha":"685c35d2096d33b757f321acd03e81de06527883","author":{"email":"fafbb143bc98b3398fb52cc5dc97b0add41e1a09@gmail.com","name":"George Karpenkov"},"message":"Bugfixes for usage of extra invariants provided by other CPAs in LPI.\n\ngit-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@17770 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c","distinct":true,"url":"https://api.github.com/repos/petr-muller/cpachecker/commits/685c35d2096d33b757f321acd03e81de06527883"},{"sha":"e298567971b9808e03c36924a5b7baee5d8181b4","author":{"email":"fafbb143bc98b3398fb52cc5dc97b0add41e1a09@gmail.com","name":"George Karpenkov"},"message":"LPI: have an option to make #getLatestVersion()  return an identity.\n\nThis is a kludge and should be removed later, fixing one option one way or the other.\n\ngit-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@17774 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c","distinct":true,"url":"https://api.github.com/repos/petr-muller/cpachecker/commits/e298567971b9808e03c36924a5b7baee5d8181b4"},{"sha":"714bd3743022f6f272842693ddcad5783d842ad1","author":{"email":"0092ec6cea8715b5650a3a96b6024d719dcbbd40@4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c","name":"ottseb"},"message":"Handle '-disable-java-assertions' in the WebClient mode of the benchmark script, too.\nImprove error message about arguments not compatible with the WebClient.\n\ngit-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@17777 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c","distinct":true,"url":"https://api.github.com/repos/petr-muller/cpachecker/commits/714bd3743022f6f272842693ddcad5783d842ad1"},{"sha":"1cd9417c853148cea521e3ee8cfd5dd4b7634168","author":{"email":"fdf48669bf30a1b7cf144e2d79bb8eed9c068d7d@4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c","name":"lukasczyk"},"message":"Activating array support with SMTInterpol solver.\n\ngit-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@17778 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c","distinct":true,"url":"https://api.github.com/repos/petr-muller/cpachecker/commits/1cd9417c853148cea521e3ee8cfd5dd4b7634168"},{"sha":"16d1ba31450093e858c4e2d91fd5791395f649e5","author":{"email":"fdf48669bf30a1b7cf144e2d79bb8eed9c068d7d@4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c","name":"lukasczyk"},"message":"Add support for arrays in counter example part for Z3 solver. \n\nThis just skips the term when having an array type, so it will not be mentioned in the counter example report. To implement this, is work in progress. Be aware of this and don't use the array theory of Z3 yet!\n\ngit-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@17782 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c","distinct":true,"url":"https://api.github.com/repos/petr-muller/cpachecker/commits/16d1ba31450093e858c4e2d91fd5791395f649e5"},{"sha":"cea91f156357573f69b4ab6b02af0f9de8e3cf59","author":{"email":"fdf48669bf30a1b7cf144e2d79bb8eed9c068d7d@4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c","name":"lukasczyk"},"message":"Add support for array formulas in Mathsat5. This is not fully working yet, do not use!\n\ngit-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@17783 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c","distinct":true,"url":"https://api.github.com/repos/petr-muller/cpachecker/commits/cea91f156357573f69b4ab6b02af0f9de8e3cf59"},{"sha":"adddabeb79d0b072168937321b9d3a1c43e80dcd","author":{"email":"ac0bf0410e278f3401f45c41c52aee879da8699a@4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c","name":"friedber"},"message":"BAM: more logging for BAM-cache\n\ngit-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@17789 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c","distinct":true,"url":"https://api.github.com/repos/petr-muller/cpachecker/commits/adddabeb79d0b072168937321b9d3a1c43e80dcd"},{"sha":"fd4dbde24a44dff9f1a8c277cdd355081f80a6d0","author":{"email":"ac0bf0410e278f3401f45c41c52aee879da8699a@4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c","name":"friedber"},"message":"BAM: redirecting map-access to helper-method.\n\ngit-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@17790 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c","distinct":true,"url":"https://api.github.com/repos/petr-muller/cpachecker/commits/fd4dbde24a44dff9f1a8c277cdd355081f80a6d0"},{"sha":"27fd250faa27d21f07be87e5c03ec8570bcd8778","author":{"email":"ac0bf0410e278f3401f45c41c52aee879da8699a@4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c","name":"friedber"},"message":"BAM: at block-exits we change the matching from path-state to reached-state.\n\nThis is a small, but important change in CEX-subgraph.\n\nWhereas the previous matching matches to a non-unique reached-state,\nwhich is expanded to several states according to its block-context,\nthe new matching uses the unique reached-state that is the expanded\nversion at the block-exit.\n\ngit-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@17791 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c","distinct":true,"url":"https://api.github.com/repos/petr-muller/cpachecker/commits/27fd250faa27d21f07be87e5c03ec8570bcd8778"},{"sha":"3b710c114b0ed7da4332da85ebe412e07c76ca87","author":{"email":"ac0bf0410e278f3401f45c41c52aee879da8699a@4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c","name":"friedber"},"message":"BAM: improving ARGSubtreeRemover.\n\nWe use the new matching of block-exit-states\nto collect the relevant definition-nodes.\nInstead of using CFAnode-based matching\nwe directly use the mapping from the BAM-Data-Mgr.\n\ngit-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@17792 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c","distinct":true,"url":"https://api.github.com/repos/petr-muller/cpachecker/commits/3b710c114b0ed7da4332da85ebe412e07c76ca87"},{"sha":"6fab7ce0db77c30bcc1175310614795ef358ec58","author":{"email":"ac0bf0410e278f3401f45c41c52aee879da8699a@4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c","name":"friedber"},"message":"BAM: simplification of loop\n\ngit-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@17797 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c","distinct":true,"url":"https://api.github.com/repos/petr-muller/cpachecker/commits/6fab7ce0db77c30bcc1175310614795ef358ec58"},{"sha":"51a67aa558eb15420d5dbc238542a844f017461a","author":{"email":"ac0bf0410e278f3401f45c41c52aee879da8699a@4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c","name":"friedber"},"message":"BAM: replace Set of Pairs by Multiset.\n\ngit-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@17798 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c","distinct":true,"url":"https://api.github.com/repos/petr-muller/cpachecker/commits/51a67aa558eb15420d5dbc238542a844f017461a"},{"sha":"e15fd60b776511b35cae4079a091a1c1e057a3db","author":{"email":"ac0bf0410e278f3401f45c41c52aee879da8699a@4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c","name":"friedber"},"message":"BAM: use BAM-Data-Mgr instead of self-collected sets of call- and exit-states.\n\ngit-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@17799 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c","distinct":true,"url":"https://api.github.com/repos/petr-muller/cpachecker/commits/e15fd60b776511b35cae4079a091a1c1e057a3db"},{"sha":"ca78d686e0b070b2bdfb813f0d430d4bb2ad6df6","author":{"email":"ac0bf0410e278f3401f45c41c52aee879da8699a@4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c","name":"friedber"},"message":"BAM: refactoring, extracting method\n\ngit-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@17800 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c","distinct":true,"url":"https://api.github.com/repos/petr-muller/cpachecker/commits/ca78d686e0b070b2bdfb813f0d430d4bb2ad6df6"},{"sha":"7802212d173d0242b5626c3c01cd56d09f6c1f07","author":{"email":"ac0bf0410e278f3401f45c41c52aee879da8699a@4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c","name":"friedber"},"message":"BAM: improving ARGSubtreeRemover, again.\n\nWe use the new matching of block-exit-states\nto collect the relevant definition-nodes.\nInstead of using CFAnode-based matching\nwe directly use the mapping from the BAM-Data-Mgr.\n\ngit-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@17801 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c","distinct":true,"url":"https://api.github.com/repos/petr-muller/cpachecker/commits/7802212d173d0242b5626c3c01cd56d09f6c1f07"},{"sha":"e7447a83a5c8d660e813e2cb64e36bef438a2c06","author":{"email":"ac0bf0410e278f3401f45c41c52aee879da8699a@4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c","name":"friedber"},"message":"BAM: fixing NullPointer.\n\ngit-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@17802 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c","distinct":true,"url":"https://api.github.com/repos/petr-muller/cpachecker/commits/e7447a83a5c8d660e813e2cb64e36bef438a2c06"},{"sha":"62c6eedc8fa34a8c53383a32b52368f39fde56dd","author":{"email":"fd754e68a8e713b5ea012d85ae703f854842758b@4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c","name":"pwendler"},"message":"Update to BenchExec 1.1\n\ngit-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@17808 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c","distinct":true,"url":"https://api.github.com/repos/petr-muller/cpachecker/commits/62c6eedc8fa34a8c53383a32b52368f39fde56dd"}]}