43 |
43 |
44 |
44 |
45 |
45 |
46 section \<open>Setup\<close> |
46 section \<open>Setup\<close> |
47 |
47 |
48 ML_file "boogie.ML" |
48 ML_file \<open>boogie.ML\<close> |
49 |
49 |
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 = true]] |
55 declare [[smt_read_only_certificates = true]] |
56 |
56 |
57 |
57 |
58 external_file "Boogie_Max.certs" |
58 external_file \<open>Boogie_Max.certs\<close> |
59 declare [[smt_certificates = "Boogie_Max.certs"]] |
59 declare [[smt_certificates = "Boogie_Max.certs"]] |
60 |
60 |
61 boogie_file Boogie_Max |
61 boogie_file \<open>Boogie_Max\<close> |
62 |
62 |
63 |
63 |
64 external_file "Boogie_Dijkstra.certs" |
64 external_file \<open>Boogie_Dijkstra.certs\<close> |
65 declare [[smt_certificates = "Boogie_Dijkstra.certs"]] |
65 declare [[smt_certificates = "Boogie_Dijkstra.certs"]] |
66 |
66 |
67 boogie_file Boogie_Dijkstra |
67 boogie_file \<open>Boogie_Dijkstra\<close> |
68 |
68 |
69 |
69 |
70 declare [[z3_extensions = true]] |
70 declare [[z3_extensions = true]] |
71 external_file "VCC_Max.certs" |
71 external_file \<open>VCC_Max.certs\<close> |
72 declare [[smt_certificates = "VCC_Max.certs"]] |
72 declare [[smt_certificates = "VCC_Max.certs"]] |
73 |
73 |
74 boogie_file VCC_Max |
74 boogie_file \<open>VCC_Max\<close> |
75 |
75 |
76 end |
76 end |