changeset 34993 | bf3b8462732b |
parent 34068 | a78307d72e58 |
child 36081 | 70deefb6c093 |
--- a/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy Tue Feb 02 18:12:05 2010 +0100 +++ b/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy Tue Feb 02 19:09:41 2010 +0100 @@ -81,9 +81,11 @@ boogie_open "~~/src/HOL/Boogie/Examples/Boogie_Dijkstra" +declare [[smt_certificates="~~/src/HOL/Boogie/Examples/Boogie_Dijkstra.certs"]] +declare [[smt_record=false]] + boogie_vc Dijkstra using [[z3_proofs=true]] - using [[smt_cert="~~/src/HOL/Boogie/Examples/cert/Boogie_Dijkstra"]] by boogie boogie_end