src/HOL/Tools/SMT/z3_replay.ML
Fri, 16 Jan 2015 23:23:31 +0100 boehmes more efficient Z3 proof reconstruction for rewrite steps with conjunctions and disjunctions, similar to Old_SMT
Thu, 15 Jan 2015 21:44:51 +0100 boehmes more detailed runtime statistics for Z3 proof reconstruction
Mon, 29 Dec 2014 22:14:13 +0100 boehmes optionally display statistics for Z3 proof reconstruction
Mon, 29 Dec 2014 14:57:13 +0100 boehmes limit reconstruction time of Z3 proof steps to be able to detect long-running reconstruction steps
Mon, 29 Sep 2014 18:37:33 +0200 blanchet simplified and repaired veriT index handling code
Thu, 28 Aug 2014 00:40:38 +0200 blanchet renamed new SMT module from 'SMT2' to 'SMT'
less more (0) tip