diff -r eaf0ffea11aa -r 446cfc760ccf src/HOL/Boogie/Examples/Boogie_Dijkstra.thy
--- a/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy	Tue Mar 27 16:59:13 2012 +0300
+++ b/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy	Tue Mar 27 16:59:13 2012 +0300
@@ -82,9 +82,9 @@
 
 boogie_open "Boogie_Dijkstra.b2i"
 
-declare [[smt_certificates="Boogie_Dijkstra.certs"]]
-declare [[smt_fixed=true]]
-declare [[smt_oracle=false]]
+declare [[smt_certificates = "Boogie_Dijkstra.certs"]]
+declare [[smt_read_only_certificates = true]]
+declare [[smt_oracle = false]]
 
 boogie_vc Dijkstra
   by boogie