more prover processes run than expected
ID0002262: This issue was created automatically from Mantis Issue 2262. Further discussion may take place here.
Id | Project | Category | View | Due Date | Updated |
---|---|---|---|---|---|
ID0002262 | Frama-C | Plug-in > wp | public | 2016-12-15 | 2016-12-16 |
Reporter | jens | Assigned To | correnson | Resolution | open |
Priority | normal | Severity | minor | Reproducibility | sometimes |
Platform | - | OS | - | OS Version | - |
Product Version | Frama-C 14-Silicon | Target Version | - | Fixed in Version | - |
Description :
When I start WP with '-wp-par 4' (for example) I often observe that more than 4 prover processes are actually running.
Additional Information :
I am not sure this is related but:
It happens from time to time that a proof obligations that is verified with '-wp-par 1' and given timeout T is not verified when using a greater number of processes and the same timeout T.
Steps To Reproduce :
run WP on example with a sufficiently large number of proof obligations that require more than one theorem prover