| changeset 48069 | e9b2782c4f99 |
| parent 47152 | 446cfc760ccf |
| child 48907 | 5c4275c3b5b8 |
--- a/src/HOL/Boogie/Examples/VCC_Max.thy Sun Jun 03 15:49:55 2012 +0200 +++ b/src/HOL/Boogie/Examples/VCC_Max.thy Mon Jun 04 09:07:23 2012 +0200 @@ -50,6 +50,7 @@ declare [[smt_certificates = "VCC_Max.certs"]] declare [[smt_read_only_certificates = true]] declare [[smt_oracle = false]] +declare [[z3_with_extensions = true]] boogie_status