equal
deleted
inserted
replaced
49 |
49 |
50 |
50 |
51 |
51 |
52 section {* Verification condition proofs *} |
52 section {* Verification condition proofs *} |
53 |
53 |
54 declare [[smt_oracle = false]] |
54 declare [[smt2_oracle = false]] |
55 declare [[smt_read_only_certificates = true]] |
55 declare [[smt2_read_only_certificates = true]] |
56 |
56 |
57 |
57 |
58 declare [[smt_certificates = "Boogie_Max.certs"]] |
58 declare [[smt2_certificates = "Boogie_Max.certs2"]] |
59 |
59 |
60 boogie_file Boogie_Max |
60 boogie_file Boogie_Max |
61 |
61 |
62 |
62 |
63 declare [[smt_certificates = "Boogie_Dijkstra.certs"]] |
63 declare [[smt2_certificates = "Boogie_Dijkstra.certs2"]] |
64 |
64 |
65 boogie_file Boogie_Dijkstra |
65 boogie_file Boogie_Dijkstra |
66 |
66 |
67 |
67 |
68 declare [[z3_with_extensions = true]] |
68 declare [[z3_new_extensions = true]] |
69 declare [[smt_certificates = "VCC_Max.certs"]] |
69 declare [[smt2_certificates = "VCC_Max.certs2"]] |
70 |
70 |
71 boogie_file VCC_Max |
71 boogie_file VCC_Max |
72 |
72 |
73 end |
73 end |