Re: SAT Solver and Improvements to the Assumptions System

2010-09-03 Thread Aaron S. Meurer
On Sep 2, 2010, at 10:24 PM, Ronan Lamy wrote: Le mercredi 25 août 2010 à 10:56 -0700, Christian Muise a écrit : Vinzent, et al, does the branch seem alright to go in at this point? I'm sitting on this merge request before bringing up the more debatable points surrounding the removal of the

Re: SAT Solver and Improvements to the Assumptions System

2010-09-03 Thread Christian Muise
It seems that this has finally been pushed in (including, unfortunately, a large mess of meaningless merges). Large mess? There shouldn't be so many since it was cleaned up with the help of Vinzent and Aaron. I think there are still a few things that should be addressed before the next

Re: SAT Solver and Improvements to the Assumptions System

2010-09-03 Thread Christian Muise
This is indeed very strange. According to issue 2046 (and my own bisecting as well) it comes from this commit: commit dcbc2da31324e98c9cb3a4bf17c50f029774ae06 Author: Sebastian Krämer basti...@gmail.com Date: Wed May 5 22:48:18 2010 +0200 Implement fast atomic substitution. *

Re: SAT Solver and Improvements to the Assumptions System

2010-09-03 Thread Aaron S. Meurer
So your merge commit 5ca928 is a merge between dcbc2d (the below commit) and e2d81ab, which is an old commit of mine. I'm not sure how that happened. Did you try doing any rebases on your history that contained merges maybe? On Sep 3, 2010, at 11:16 AM, Christian Muise wrote: This is indeed

Re: SAT Solver and Improvements to the Assumptions System

2010-09-03 Thread Christian Muise
So your merge commit 5ca928 is a merge between dcbc2d (the below commit) and e2d81ab, which is an old commit of mine. I'm not sure how that happened. Did you try doing any rebases on your history that contained merges maybe? I don't believe so, but that span of 3 days is quite muddled

Re: SAT Solver and Improvements to the Assumptions System

2010-09-03 Thread Ondrej Certik
Hi, I have pushed this in, so the blame goes to my head. Some comments: On Fri, Sep 3, 2010 at 10:16 AM, Christian Muise christian.mu...@gmail.com wrote: This is indeed very strange.  According to issue 2046 (and my own bisecting as well) it comes from this commit: commit

Re: SAT Solver and Improvements to the Assumptions System

2010-09-03 Thread Aaron S. Meurer
On Sep 3, 2010, at 4:21 PM, Ondrej Certik wrote: Hi, I have pushed this in, so the blame goes to my head. Some comments: On Fri, Sep 3, 2010 at 10:16 AM, Christian Muise christian.mu...@gmail.com wrote: This is indeed very strange. According to issue 2046 (and my own bisecting as well)

Re: SAT Solver and Improvements to the Assumptions System

2010-09-03 Thread Ondrej Certik
On Fri, Sep 3, 2010 at 3:50 PM, Aaron S. Meurer asmeu...@gmail.com wrote: On Sep 3, 2010, at 4:21 PM, Ondrej Certik wrote: Hi, I have pushed this in, so the blame goes to my head. Some comments: On Fri, Sep 3, 2010 at 10:16 AM, Christian Muise christian.mu...@gmail.com wrote: This is