src/HOL/SMT_Examples/Boogie.thy
changeset 66758 9312ce5a938d
parent 66741 c90fb8bee1dd
child 69605 a96320074298
equal deleted inserted replaced
66757:e32750d7acb4 66758:9312ce5a938d
    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 external_file "Boogie_Max.certs"
    58 declare [[smt_certificates = "Boogie_Max.certs"]]
    59 declare [[smt_certificates = "Boogie_Max.certs"]]
    59 
    60 
    60 boogie_file Boogie_Max
    61 boogie_file Boogie_Max
    61 
    62 
    62 
    63 
       
    64 external_file "Boogie_Dijkstra.certs"
    63 declare [[smt_certificates = "Boogie_Dijkstra.certs"]]
    65 declare [[smt_certificates = "Boogie_Dijkstra.certs"]]
    64 
    66 
    65 boogie_file Boogie_Dijkstra
    67 boogie_file Boogie_Dijkstra
    66 
    68 
    67 
    69 
    68 declare [[z3_extensions = true]]
    70 declare [[z3_extensions = true]]
       
    71 external_file "VCC_Max.certs"
    69 declare [[smt_certificates = "VCC_Max.certs"]]
    72 declare [[smt_certificates = "VCC_Max.certs"]]
    70 
    73 
    71 boogie_file VCC_Max
    74 boogie_file VCC_Max
    72 
    75 
    73 end
    76 end