{"push_id":1156428569,"size":17,"distinct_size":8,"ref":"refs/heads/master","head":"c7ff05cc78f90f3b10901e4efb5ba8be85246915","before":"9df2a183d6972cb408e88a3d3d245d0a2cfe45ce","commits":[{"sha":"219b47822b8912c1d8846820635589cf12d25dbb","author":{"name":"Nikolaj Bjorner","email":"33a8e74d98f5ce989605ca1273b437c997827c25@microsoft.com"},"message":"avoid qsat when formulas are quantifier-free. Go directly to SMT\n\nSigned-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>","distinct":false,"url":"https://api.github.com/repos/MikolasJanota/z3/commits/219b47822b8912c1d8846820635589cf12d25dbb"},{"sha":"19db0c5f2cba896e2aa15761c43b4d5ddfb68e1a","author":{"name":"Nikolaj Bjorner","email":"33a8e74d98f5ce989605ca1273b437c997827c25@microsoft.com"},"message":"Merge branch 'master' of https://github.com/Z3Prover/z3","distinct":false,"url":"https://api.github.com/repos/MikolasJanota/z3/commits/19db0c5f2cba896e2aa15761c43b4d5ddfb68e1a"},{"sha":"47f97dde8940fac120da1dbd934d5cd52a34db3c","author":{"name":"Nikolaj Bjorner","email":"33a8e74d98f5ce989605ca1273b437c997827c25@microsoft.com"},"message":"Merge pull request #639 from MikolasJanota/master\n\nAdding translation to ackr_model_converter.","distinct":false,"url":"https://api.github.com/repos/MikolasJanota/z3/commits/47f97dde8940fac120da1dbd934d5cd52a34db3c"},{"sha":"9bfa73ee062370b35eb0dedc9611b6443f83939b","author":{"name":"Johannes Kanig","email":"19a95c91d399ff8c1bef037aa1b7ab3a4ac47970@adacore.com"},"message":"Take into account number of monomials for rlimit counting\n\nShould fix issue #611","distinct":false,"url":"https://api.github.com/repos/MikolasJanota/z3/commits/9bfa73ee062370b35eb0dedc9611b6443f83939b"},{"sha":"314eae50a450b9e0196a14d55998eedd555022cf","author":{"name":"Nikolaj Bjorner","email":"33a8e74d98f5ce989605ca1273b437c997827c25@microsoft.com"},"message":"Merge pull request #641 from kanigsson/master\n\nTake into account number of monomials for rlimit counting","distinct":false,"url":"https://api.github.com/repos/MikolasJanota/z3/commits/314eae50a450b9e0196a14d55998eedd555022cf"},{"sha":"a2eb8245900c84607c7e55ac501b75fb6d0407dd","author":{"name":"Christoph M. Wintersteiger","email":"564cdc231b061157d41da4fa6ebb9f0cd1020917@microsoft.com"},"message":"Added __nonzero__ and __bool__ functions to Python Z3 ASTs to enable use of Python lists (and similar).\n\nThanks to Vlad Shcherbina for the recommendation (see http://stackoverflow.com/questions/37669576/converting-z3-cnf-formula-into-list-of-lists-representation-using-z3py/37679447?noredirect=1#comment62859886_37679447)!","distinct":false,"url":"https://api.github.com/repos/MikolasJanota/z3/commits/a2eb8245900c84607c7e55ac501b75fb6d0407dd"},{"sha":"9b91e6ff0aa6d3ca759a61b701f987e71eb04540","author":{"name":"Christoph M. Wintersteiger","email":"564cdc231b061157d41da4fa6ebb9f0cd1020917@microsoft.com"},"message":"Merge branch 'master' of https://github.com/Z3Prover/z3","distinct":false,"url":"https://api.github.com/repos/MikolasJanota/z3/commits/9b91e6ff0aa6d3ca759a61b701f987e71eb04540"},{"sha":"5253f3a12b36821a9c2a84bc604540689d80ddff","author":{"name":"Nikolaj Bjorner","email":"33a8e74d98f5ce989605ca1273b437c997827c25@microsoft.com"},"message":"internalize unsupported operations\n\nSigned-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>","distinct":false,"url":"https://api.github.com/repos/MikolasJanota/z3/commits/5253f3a12b36821a9c2a84bc604540689d80ddff"},{"sha":"cb29c07f067133bf8d09c2b3152e85a9d9180332","author":{"name":"Nikolaj Bjorner","email":"33a8e74d98f5ce989605ca1273b437c997827c25@microsoft.com"},"message":"Merge branch 'master' of https://github.com/Z3Prover/z3","distinct":false,"url":"https://api.github.com/repos/MikolasJanota/z3/commits/cb29c07f067133bf8d09c2b3152e85a9d9180332"},{"sha":"879363157f008d8e635f7c4a66c12c241640e8b6","author":{"name":"Christoph M. Wintersteiger","email":"564cdc231b061157d41da4fa6ebb9f0cd1020917@microsoft.com"},"message":"Bugfix for fpa2bv_converter","distinct":true,"url":"https://api.github.com/repos/MikolasJanota/z3/commits/879363157f008d8e635f7c4a66c12c241640e8b6"},{"sha":"bfeab9cc154dc93547d67aee36e6210f2fa6638c","author":{"name":"Christoph M. Wintersteiger","email":"564cdc231b061157d41da4fa6ebb9f0cd1020917@microsoft.com"},"message":"Added facilities for hiding UFs in smt::model_generator","distinct":true,"url":"https://api.github.com/repos/MikolasJanota/z3/commits/bfeab9cc154dc93547d67aee36e6210f2fa6638c"},{"sha":"bd187e098988c57b5dc8e75480c42717ffeb3482","author":{"name":"Christoph M. Wintersteiger","email":"564cdc231b061157d41da4fa6ebb9f0cd1020917@microsoft.com"},"message":"Bugfix for fp.min/fp.max in fpa2bv converter; hide BV UFs from FP models.\n\nFixes #642","distinct":true,"url":"https://api.github.com/repos/MikolasJanota/z3/commits/bd187e098988c57b5dc8e75480c42717ffeb3482"},{"sha":"19f98547f7d3155f4a8985a068f5171f9e16a090","author":{"name":"Nikolaj Bjorner","email":"33a8e74d98f5ce989605ca1273b437c997827c25@microsoft.com"},"message":"fix memory leak Issue #643\n\nSigned-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>","distinct":true,"url":"https://api.github.com/repos/MikolasJanota/z3/commits/19f98547f7d3155f4a8985a068f5171f9e16a090"},{"sha":"9f5a117443122bfac118a73475f67bbb45adc4a4","author":{"name":"Nikolaj Bjorner","email":"33a8e74d98f5ce989605ca1273b437c997827c25@microsoft.com"},"message":"move mus to solver\n\nSigned-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>","distinct":true,"url":"https://api.github.com/repos/MikolasJanota/z3/commits/9f5a117443122bfac118a73475f67bbb45adc4a4"},{"sha":"ea201a776d09b889c76b3822b3d08a944e8ea8d4","author":{"name":"Nikolaj Bjorner","email":"33a8e74d98f5ce989605ca1273b437c997827c25@microsoft.com"},"message":"enable qsat-opt\n\nSigned-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>","distinct":true,"url":"https://api.github.com/repos/MikolasJanota/z3/commits/ea201a776d09b889c76b3822b3d08a944e8ea8d4"},{"sha":"3ac47099921543aa174fb3fb3641645efc62660b","author":{"name":"Nikolaj Bjorner","email":"33a8e74d98f5ce989605ca1273b437c997827c25@microsoft.com"},"message":"Merge branch 'master' of https://github.com/Z3Prover/z3","distinct":true,"url":"https://api.github.com/repos/MikolasJanota/z3/commits/3ac47099921543aa174fb3fb3641645efc62660b"},{"sha":"c7ff05cc78f90f3b10901e4efb5ba8be85246915","author":{"name":"Nikolaj Bjorner","email":"33a8e74d98f5ce989605ca1273b437c997827c25@microsoft.com"},"message":"enable core minimization with qsat in case it turns out to be useful\n\nSigned-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>","distinct":true,"url":"https://api.github.com/repos/MikolasJanota/z3/commits/c7ff05cc78f90f3b10901e4efb5ba8be85246915"}]}
{"actor":{"display_login":"MikolasJanota"}}