Fri, 11 Mar 2011 08:58:29 +0100 removing debug message in quickcheck's postprocessor
bulwahn [Fri, 11 Mar 2011 08:58:29 +0100] rev 41904
removing debug message in quickcheck's postprocessor
Fri, 11 Mar 2011 08:13:00 +0100 fixing postprocessing; adding a configuration to enable and disable pretty presentation of quickcheck's counterexample
bulwahn [Fri, 11 Mar 2011 08:13:00 +0100] rev 41903
fixing postprocessing; adding a configuration to enable and disable pretty presentation of quickcheck's counterexample
Fri, 11 Mar 2011 08:12:59 +0100 renaming dest_plain_fun to dest_fun_upds and adding handling of undefined for postprocessing of quickcheck
bulwahn [Fri, 11 Mar 2011 08:12:59 +0100] rev 41902
renaming dest_plain_fun to dest_fun_upds and adding handling of undefined for postprocessing of quickcheck
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
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip