overly generic logics declaration causes slowdown of cvc4 proof
Florian had identified a long time ago an issue where cvc4 would take much longer to prove a given VC if a non-linear arithmetic was specified compared to a linear one. See this ticket and the example in the ticket:
https://github.com/CVC4/CVC4/issues/1276
On my machine, there is a factor of 10 (0.6s vs 6s) between UFBVDTLIRA and UFBVDTNIRA when using cvc4 on the example in the issue.
We were wondering if Why3 could be more precise, e.g. detecting when only linear operators are used. Given the potentially large speedups it seems worthwhile. The other idea mentioned in the TN to specify --inst-when-strict-interleave isn't an option for us.
To upload designs, you'll need to enable LFS. More information