Strange timing for valid VCs in portfolio mode with timeout

epfl-lara / stainless

Verification framework and tool for higher-order Scala programs

https://epfl-lara.github.io/stainless/

Apache License 2.0

359 stars 53 forks source link

Strange timing for valid VCs in portfolio mode with timeout #980

Open jad-hamza opened 3 years ago

jad-hamza commented 3 years ago

Running the example from https://github.com/epfl-lara/stainless/issues/979 in portfolio mode with --vc-cache=false --solvers=smt-z3,smt-cvc4 --timeout=N takes around N seconds (+loading) and succeeds with the (body assertion) VC being verified in exactly N seconds. I tried with N = 10, N = 18, N = 24, or N = 100, and the VC consistently takes N seconds to be verified. I wonder if perhaps the VC is displayed as valid while it's actually timing out.

jad-hamza commented 3 years ago

I checked again by running just with --solvers=smt-cvc4, and CVC4 is in fact able to solve the VC instantly (so last sentence of previous post was wrong). But for some reason the portfolio solver keeps on running until the timeout.

jad-hamza commented 3 years ago

Fixed in https://github.com/epfl-lara/inox/pull/134