blanchet [Sun, 07 Nov 2010 17:51:25 +0100] rev 40412
if SMT used as a filter in a loop fails at each iteration, returns the first error, not the last, since it is more informative -- the first error typically says "out of memory", whereas the last might well be "the SMT problem is unprovable", which should be no surprise if too many facts were removed
blanchet [Sun, 07 Nov 2010 13:29:59 +0100] rev 40411
removed explicit "Interrupt" handling for conformity with async model -- unfortunately the user loses the information about how many scopes were checked, but this needs to be retought with the new interface anyway