Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Last revision Both sides next revision | ||
|
bank_account_example_in_jahob [2007/05/14 12:36] vkuncak |
bank_account_example_in_jahob [2007/05/14 12:36] vkuncak |
||
|---|---|---|---|
| Line 7: | Line 7: | ||
| The command to verify this example is | The command to verify this example is | ||
| ../../bin/jahob.opt Account.java -class Account -sastvc -usedp cvcl | ../../bin/jahob.opt Account.java -class Account -sastvc -usedp cvcl | ||
| - | and requires an SMT-LIB solver under the name 'cvcl' to be installed to work. | + | and requires an SMT-LIB solver under the name 'cvcl' to be installed to work (download[[http://www.cs.nyu.edu/acsys/cvc3/|CVC3]] and create a symlink to that executable). |
| <code java> | <code java> | ||