Time-out with satisfiable problems in SMT-LIB2 about vampire HOT 2 CLOSED

Unfortunately this doesn't seem like a bug. Vampire will occasionally terminate on satisfiable instances, but it's not necessarily very good at it, as in this case. Models don't work either, because we don't usually build models. You might consider using e.g. a portfolio of Vampire and Z3 for both satisfiable and unsatisfiable instances.

from vampire.

I just wanted to add. Vampire will never report SAT if the input has arithmetic in it that can't be trivially removed during preprocessing as as soon as we see arithmetic we will mark saturation as incomplete.

We could be more aggressive with that (e.g. we could support the above problem) but satisfiability with interpreted theories isn't something we put effort into supporting. If that's something you want then you should use an SMT solver.

There was once an option to pass ground input directly through to our wrapped SMT solver. We could reintroduce this, but again, it isn't going to give any better results than using an SMT solver directly.

from vampire.