equal
deleted
inserted
replaced
80 |
80 |
81 |
81 |
82 boogie_open "~~/src/HOL/Boogie/Examples/Boogie_Dijkstra" |
82 boogie_open "~~/src/HOL/Boogie/Examples/Boogie_Dijkstra" |
83 |
83 |
84 declare [[smt_certificates="~~/src/HOL/Boogie/Examples/Boogie_Dijkstra.certs"]] |
84 declare [[smt_certificates="~~/src/HOL/Boogie/Examples/Boogie_Dijkstra.certs"]] |
85 declare [[smt_record=false]] |
85 declare [[smt_fixed=true]] |
86 |
86 |
87 boogie_vc Dijkstra |
87 boogie_vc Dijkstra |
88 using [[z3_proofs=true]] |
88 using [[z3_proofs=true]] |
89 by boogie |
89 by boogie |
90 |
90 |