src/HOL/SMT_Examples/Boogie.thy
changeset 66758 9312ce5a938d
parent 66741 c90fb8bee1dd
child 69605 a96320074298
     1.1 --- a/src/HOL/SMT_Examples/Boogie.thy	Mon Oct 02 19:28:18 2017 +0200
     1.2 +++ b/src/HOL/SMT_Examples/Boogie.thy	Mon Oct 02 19:38:39 2017 +0200
     1.3 @@ -55,17 +55,20 @@
     1.4  declare [[smt_read_only_certificates = true]]
     1.5  
     1.6  
     1.7 +external_file "Boogie_Max.certs"
     1.8  declare [[smt_certificates = "Boogie_Max.certs"]]
     1.9  
    1.10  boogie_file Boogie_Max
    1.11  
    1.12  
    1.13 +external_file "Boogie_Dijkstra.certs"
    1.14  declare [[smt_certificates = "Boogie_Dijkstra.certs"]]
    1.15  
    1.16  boogie_file Boogie_Dijkstra
    1.17  
    1.18  
    1.19  declare [[z3_extensions = true]]
    1.20 +external_file "VCC_Max.certs"
    1.21  declare [[smt_certificates = "VCC_Max.certs"]]
    1.22  
    1.23  boogie_file VCC_Max