1.1 --- a/src/HOL/Boogie/Examples/VCC_Max.thy	Sun Jun 03 15:49:55 2012 +0200
     1.2 +++ b/src/HOL/Boogie/Examples/VCC_Max.thy	Mon Jun 04 09:07:23 2012 +0200
     1.3 @@ -50,6 +50,7 @@
     1.4  declare [[smt_certificates = "VCC_Max.certs"]]
     1.5  declare [[smt_read_only_certificates = true]]
     1.6  declare [[smt_oracle = false]]
     1.7 +declare [[z3_with_extensions = true]]
     1.8  
     1.9  boogie_status
    1.10