Fri, 01 Apr 2011 15:49:19 +0200 save reflexivity steps in discharging Z3 Skolemization hypotheses
boehmes [Fri, 01 Apr 2011 15:49:19 +0200] rev 42196
save reflexivity steps in discharging Z3 Skolemization hypotheses
Fri, 01 Apr 2011 13:49:38 +0200 adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn [Fri, 01 Apr 2011 13:49:38 +0200] rev 42195
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
Fri, 01 Apr 2011 13:49:36 +0200 adding general interface for batch validators in quickcheck
bulwahn [Fri, 01 Apr 2011 13:49:36 +0200] rev 42194
adding general interface for batch validators in quickcheck
Fri, 01 Apr 2011 13:21:21 +0200 remove workaround 8f25605e646c, which is no longer necessary thanks to 173b0f488428
blanchet [Fri, 01 Apr 2011 13:21:21 +0200] rev 42193
remove workaround 8f25605e646c, which is no longer necessary thanks to 173b0f488428
Fri, 01 Apr 2011 12:19:54 +0200 scheduler for judgement day
krauss [Fri, 01 Apr 2011 12:19:54 +0200] rev 42192
scheduler for judgement day
Fri, 01 Apr 2011 12:16:41 +0200 re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes [Fri, 01 Apr 2011 12:16:41 +0200] rev 42191
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
Fri, 01 Apr 2011 11:54:51 +0200 make configuration of (SMT) full monomorphization more flexible: turn boolean argument into a configuration option
boehmes [Fri, 01 Apr 2011 11:54:51 +0200] rev 42190
make configuration of (SMT) full monomorphization more flexible: turn boolean argument into a configuration option
Fri, 01 Apr 2011 10:18:20 +0200 merged
bulwahn [Fri, 01 Apr 2011 10:18:20 +0200] rev 42189
merged
Fri, 01 Apr 2011 09:20:59 +0200 adding time profiling in quickcheck's batch testing for further diagnosis in IsaCoSy
bulwahn [Fri, 01 Apr 2011 09:20:59 +0200] rev 42188
adding time profiling in quickcheck's batch testing for further diagnosis in IsaCoSy
Fri, 01 Apr 2011 09:48:01 +0200 raised timeouts further, for SML/NJ
krauss [Fri, 01 Apr 2011 09:48:01 +0200] rev 42187
raised timeouts further, for SML/NJ
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip