equal
deleted
inserted
replaced
36 \end{verbatim} |
36 \end{verbatim} |
37 *} |
37 *} |
38 |
38 |
39 boogie_open "~~/src/HOL/Boogie/Examples/Boogie_Max" |
39 boogie_open "~~/src/HOL/Boogie/Examples/Boogie_Max" |
40 |
40 |
|
41 declare [[smt_certificates="~~/src/HOL/Boogie/Examples/Boogie_Max.certs"]] |
|
42 declare [[smt_record=false]] |
|
43 |
41 boogie_vc max |
44 boogie_vc max |
42 using [[z3_proofs=true]] |
45 using [[z3_proofs=true]] |
43 using [[smt_cert="~~/src/HOL/Boogie/Examples/cert/Boogie_max"]] |
|
44 by boogie |
46 by boogie |
45 |
47 |
46 boogie_end |
48 boogie_end |
47 |
49 |
48 end |
50 end |