changeset 66740 | ece9435ca78e |
parent 63167 | 0909deb8059b |
child 66741 | c90fb8bee1dd |
--- a/src/HOL/SMT_Examples/Boogie.thy Sun Oct 01 15:17:31 2017 +0200 +++ b/src/HOL/SMT_Examples/Boogie.thy Sun Oct 01 15:17:43 2017 +0200 @@ -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]] (* FIXME *) declare [[smt_certificates = "Boogie_Max.certs"]]