search

vprover / vampire

The Vampire Theorem Prover
https://vprover.github.io/
Other
282 stars 49 forks source link

bad test id errors #576

Closed joe-hauns closed 1 month ago

joe-hauns commented 2 months ago

Running vampire with the portfolio snake_tptp_uns all over smtlib and tptp gives quite some user errors of the shape bad test id ins+<strategy-string>. This is due to the removal of the ins saturation algorithm, which is still present in the schedule. What do you think we should do about this? Should we just remove all these strategies from the schedules?

quickbeam123 commented 2 months ago

Sure, the ins strategies make no sense there anymore.

Please also note that snake_tptp_uns does not know anything about the SMTLIB logics etc, so the strategy dispatch could be quite broken there.