wenzelm [Sat, 13 Nov 2010 12:32:21 +0100] rev 40521
back to quick_and_dirty, which is still practically important since the scheduler does not jump over subproofs;
wenzelm [Sat, 13 Nov 2010 11:41:02 +0100] rev 40520
await_cancellation in the main thread, independently of the execution futures, which might get interrupted or be absent after node deletetion;
wenzelm [Sat, 13 Nov 2010 00:24:41 +0100] rev 40519
updated README;
wenzelm [Fri, 12 Nov 2010 21:37:01 +0100] rev 40518
defensive defaults for more robust experience for new users;
wenzelm [Fri, 12 Nov 2010 17:44:03 +0100] rev 40517
merged
boehmes [Fri, 12 Nov 2010 15:56:11 +0100] rev 40516
preliminary support for newer versions of Z3
boehmes [Fri, 12 Nov 2010 15:56:10 +0100] rev 40515
turned SMT counterexamples into verbose messages (they had been swallowed before, following the state of smt_trace -- which is off by default), because they might be useful for the user
boehmes [Fri, 12 Nov 2010 15:56:08 +0100] rev 40514
let the theory formally depend on the Boogie output
boehmes [Fri, 12 Nov 2010 15:56:07 +0100] rev 40513
look for certificates relative to the theory
boehmes [Fri, 12 Nov 2010 15:56:06 +0100] rev 40512
dropped numerals from monomorphization blacklist (only particular numerals are builtin, all other numerals should be treated uninterpreted), this blacklist should contain only truely polymorphic builtin constants supported by SMT