src/HOL/Boogie/Examples/Boogie_Dijkstra.thy
changeset 40163 a462d5207aa6
parent 36081 70deefb6c093
child 40513 1204d268464f
     1.1 --- a/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy	Tue Oct 26 11:45:12 2010 +0200
     1.2 +++ b/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy	Tue Oct 26 11:46:19 2010 +0200
     1.3 @@ -83,9 +83,9 @@
     1.4  
     1.5  declare [[smt_certificates="~~/src/HOL/Boogie/Examples/Boogie_Dijkstra.certs"]]
     1.6  declare [[smt_fixed=true]]
     1.7 +declare [[smt_oracle=false]]
     1.8  
     1.9  boogie_vc Dijkstra
    1.10 -  using [[z3_proofs=true]]
    1.11    by boogie
    1.12  
    1.13  boogie_end