--- 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