158 dramatically improved. |
158 dramatically improved. |
159 - Improved support for CVC4 and veriT. |
159 - Improved support for CVC4 and veriT. |
160 |
160 |
161 * Old and new SMT modules: |
161 * Old and new SMT modules: |
162 - The old 'smt' method has been renamed 'old_smt' and moved to |
162 - The old 'smt' method has been renamed 'old_smt' and moved to |
163 'src/HOL/Library/Old_SMT.thy'. It provided for compatibility, until |
163 'src/HOL/Library/Old_SMT.thy'. It is provided for compatibility, until |
164 applications have been ported to use the new 'smt' method. For the |
164 applications have been ported to use the new 'smt' method. For the |
165 method to work, an older version of Z3 (e.g. Z3 3.2 or 4.0) must be |
165 method to work, an older version of Z3 (e.g. Z3 3.2 or 4.0) must be |
166 installed, and the environment variable "OLD_Z3_SOLVER" must point to |
166 installed, and the environment variable "OLD_Z3_SOLVER" must point to |
167 it. |
167 it. |
168 INCOMPATIBILITY. |
168 INCOMPATIBILITY. |
169 - The 'smt2' method has been renamed 'smt'. |
169 - The 'smt2' method has been renamed 'smt'. |
170 INCOMPATIBILITY. |
170 INCOMPATIBILITY. |
|
171 - New option 'smt_reconstruction_step_timeout' to limit the reconstruction |
|
172 time of Z3 proof steps in the new 'smt' method. |
|
173 - New option 'smt_statistics' to display statistics of the new 'smt' |
|
174 method, especially runtime statistics of Z3 proof reconstruction. |
171 |
175 |
172 * List: renamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc |
176 * List: renamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc |
173 |
177 |
174 * New infrastructure for compiling, running, evaluating and testing |
178 * New infrastructure for compiling, running, evaluating and testing |
175 generated code in target languages in HOL/Library/Code_Test. See |
179 generated code in target languages in HOL/Library/Code_Test. See |