equal
deleted
inserted
replaced
50 |
50 |
51 |
51 |
52 section \<open>Verification condition proofs\<close> |
52 section \<open>Verification condition proofs\<close> |
53 |
53 |
54 declare [[smt_oracle = false]] |
54 declare [[smt_oracle = false]] |
55 declare [[smt_read_only_certificates = false]] (* FIXME *) |
55 declare [[smt_read_only_certificates = true]] |
56 |
56 |
57 |
57 |
58 declare [[smt_certificates = "Boogie_Max.certs"]] |
58 declare [[smt_certificates = "Boogie_Max.certs"]] |
59 |
59 |
60 boogie_file Boogie_Max |
60 boogie_file Boogie_Max |