--- Isabelle2016-1-orig/src/HOL/SMT_Examples/Boogie.thy	2016-12-13 01:03:38.000000000 +1100
+++ Isabelle2016-1/src/HOL/SMT_Examples/Boogie.thy	2016-12-30 23:46:11.947737290 +1100
@@ -52,7 +52,7 @@
 section \<open>Verification condition proofs\<close>
 
 declare [[smt_oracle = false]]
-declare [[smt_read_only_certificates = true]]
+declare [[smt_read_only_certificates = false]]
 
 
 declare [[smt_certificates = "Boogie_Max.certs"]]
--- Isabelle2016-1-orig/src/HOL/SMT_Examples/SMT_Examples.thy	2016-12-13 01:03:38.000000000 +1100
+++ Isabelle2016-1/src/HOL/SMT_Examples/SMT_Examples.thy	2016-12-30 23:46:11.953737338 +1100
@@ -9,7 +9,7 @@
 begin
 
 declare [[smt_certificates = "SMT_Examples.certs"]]
-declare [[smt_read_only_certificates = true]]
+declare [[smt_read_only_certificates = false]]
 
 
 section \<open>Propositional and first-order logic\<close>
--- Isabelle2016-1-orig/src/HOL/SMT_Examples/SMT_Word_Examples.thy	2016-12-13 01:03:38.000000000 +1100
+++ Isabelle2016-1/src/HOL/SMT_Examples/SMT_Word_Examples.thy	2016-12-30 23:46:11.967737450 +1100
@@ -11,7 +11,7 @@
 declare [[smt_oracle = true]]
 declare [[z3_extensions = true]]
 declare [[smt_certificates = "SMT_Word_Examples.certs"]]
-declare [[smt_read_only_certificates = true]]
+declare [[smt_read_only_certificates = false]]
 
 text \<open>
 Currently, there is no proof reconstruction for words.