src/HOL/SMT_Examples/Boogie.thy
changeset 58367 8af1e68d7e1a
parent 58061 3d060f43accb
child 58889 5b7a9633cfa8
equal deleted inserted replaced
58366:5cf7df52d71d 58367:8af1e68d7e1a
    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 declare [[smt_certificates = "Boogie_Max.certs2"]]
    58 declare [[smt_certificates = "Boogie_Max.certs"]]
    59 
    59 
    60 boogie_file Boogie_Max
    60 boogie_file Boogie_Max
    61 
    61 
    62 
    62 
    63 declare [[smt_certificates = "Boogie_Dijkstra.certs2"]]
    63 declare [[smt_certificates = "Boogie_Dijkstra.certs"]]
    64 
    64 
    65 boogie_file Boogie_Dijkstra
    65 boogie_file Boogie_Dijkstra
    66 
    66 
    67 
    67 
    68 declare [[z3_extensions = true]]
    68 declare [[z3_extensions = true]]
    69 declare [[smt_certificates = "VCC_Max.certs2"]]
    69 declare [[smt_certificates = "VCC_Max.certs"]]
    70 
    70 
    71 boogie_file VCC_Max
    71 boogie_file VCC_Max
    72 
    72 
    73 end
    73 end