| changeset 40514 | db5f14910dce |
| parent 40513 | 1204d268464f |
| child 40540 | 293f9f211be0 |
| 40513:1204d268464f | 40514:db5f14910dce |
|---|---|
34 } |
34 } |
35 } |
35 } |
36 \end{verbatim} |
36 \end{verbatim} |
37 *} |
37 *} |
38 |
38 |
39 boogie_open "~~/src/HOL/Boogie/Examples/Boogie_Max" |
39 boogie_open "Boogie_Max" |
40 |
40 |
41 declare [[smt_certificates="Boogie_Max.certs"]] |
41 declare [[smt_certificates="Boogie_Max.certs"]] |
42 declare [[smt_fixed=true]] |
42 declare [[smt_fixed=true]] |
43 declare [[smt_oracle=false]] |
43 declare [[smt_oracle=false]] |
44 |
44 |