| changeset 47152 | 446cfc760ccf |
| parent 41601 | fda8511006f9 |
| child 48069 | e9b2782c4f99 |
--- a/src/HOL/Boogie/Examples/VCC_Max.thy Tue Mar 27 16:59:13 2012 +0300 +++ b/src/HOL/Boogie/Examples/VCC_Max.thy Tue Mar 27 16:59:13 2012 +0300 @@ -47,9 +47,9 @@ boogie_open (quiet) "VCC_Max.b2i" -declare [[smt_certificates="VCC_Max.certs"]] -declare [[smt_fixed=true]] -declare [[smt_oracle=false]] +declare [[smt_certificates = "VCC_Max.certs"]] +declare [[smt_read_only_certificates = true]] +declare [[smt_oracle = false]] boogie_status