Skip to content

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

Attachments

  • screen-shot
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information