Fri, 11 Mar 2011 08:12:58 +0100 improving term postprocessing for counterexample presentation in quickcheck
bulwahn [Fri, 11 Mar 2011 08:12:58 +0100] rev 41901
improving term postprocessing for counterexample presentation in quickcheck
Fri, 11 Mar 2011 08:12:55 +0100 tuned
bulwahn [Fri, 11 Mar 2011 08:12:55 +0100] rev 41900
tuned
Wed, 09 Mar 2011 21:40:38 +0100 finished and tested Z3 proof reconstruction for injective functions;
boehmes [Wed, 09 Mar 2011 21:40:38 +0100] rev 41899
finished and tested Z3 proof reconstruction for injective functions; only treat variables as atomic, and especially abstract constants (Isabelle's interpretation of these constants is most likely not known to Z3 and thus irrelevant for the proof)
Wed, 09 Mar 2011 10:28:01 +0100 improved formula for specialization, to prevent needless specializations -- and removed dead code
blanchet [Wed, 09 Mar 2011 10:28:01 +0100] rev 41898
improved formula for specialization, to prevent needless specializations -- and removed dead code
Wed, 09 Mar 2011 10:25:29 +0100 perform no arity check in debug mode so that we get to see the Kodkod problem
blanchet [Wed, 09 Mar 2011 10:25:29 +0100] rev 41897
perform no arity check in debug mode so that we get to see the Kodkod problem
Fri, 04 Mar 2011 17:39:30 +0100 spark_end now joins proofs of VCs before writing *.prv file.
berghofe [Fri, 04 Mar 2011 17:39:30 +0100] rev 41896
spark_end now joins proofs of VCs before writing *.prv file.
Fri, 04 Mar 2011 11:43:20 +0100 clarified
krauss [Fri, 04 Mar 2011 11:43:20 +0100] rev 41895
clarified
Fri, 04 Mar 2011 11:52:54 +0100 produce helpful mira summary for more errors
krauss [Fri, 04 Mar 2011 11:52:54 +0100] rev 41894
produce helpful mira summary for more errors
Fri, 04 Mar 2011 00:09:47 +0100 eliminated prems;
wenzelm [Fri, 04 Mar 2011 00:09:47 +0100] rev 41893
eliminated prems;
Thu, 03 Mar 2011 22:06:15 +0100 eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;
wenzelm [Thu, 03 Mar 2011 22:06:15 +0100] rev 41892
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip