Inefficiency in checking contract against implementation
At present OCRA gives an error (segmentation fault) if we try to pass the contract for implementation with -C option. So, at present for implementation all the contracts in the specification file are verified.
This results in inefficiency as demonstrated by the following example:
Consider a component with 5 contracts. This results in 5 "constraints". Now due to above mentioned problem the total number of verified contracts is 25 (5 * 5). This results in inefficient implementation. Now, either this should be resolved by fbk or we should adapt our implementation.