diff -r e32750d7acb4 -r 9312ce5a938d src/HOL/SMT_Examples/Boogie.thy
--- a/src/HOL/SMT_Examples/Boogie.thy	Mon Oct 02 19:28:18 2017 +0200
+++ b/src/HOL/SMT_Examples/Boogie.thy	Mon Oct 02 19:38:39 2017 +0200
@@ -55,17 +55,20 @@
 declare [[smt_read_only_certificates = true]]
 
 
+external_file "Boogie_Max.certs"
 declare [[smt_certificates = "Boogie_Max.certs"]]
 
 boogie_file Boogie_Max
 
 
+external_file "Boogie_Dijkstra.certs"
 declare [[smt_certificates = "Boogie_Dijkstra.certs"]]
 
 boogie_file Boogie_Dijkstra
 
 
 declare [[z3_extensions = true]]
+external_file "VCC_Max.certs"
 declare [[smt_certificates = "VCC_Max.certs"]]
 
 boogie_file VCC_Max