changeset 34993 | bf3b8462732b |
parent 34068 | a78307d72e58 |
child 35153 | 5e8935678ee4 |
--- a/src/HOL/Boogie/Examples/VCC_Max.thy Tue Feb 02 18:12:05 2010 +0100 +++ b/src/HOL/Boogie/Examples/VCC_Max.thy Tue Feb 02 19:09:41 2010 +0100 @@ -46,11 +46,13 @@ boogie_open (quiet) "~~/src/HOL/Boogie/Examples/VCC_Max" +declare [[smt_certificates="~~/src/HOL/Boogie/Examples/VCC_Max.certs"]] +declare [[smt_record=false]] + boogie_status boogie_vc maximum using [[z3_proofs=true]] - using [[smt_cert="~~/src/HOL/Boogie/Examples/cert/VCC_maximum"]] by boogie boogie_end