Time-out with satisfiable problems in SMT-LIB2

[KJanelle]

When trying to solve trivial satisfiable problems like the following, I always run into a time-out:

(set-logic ALL)
(declare-const y Int)
(assert (= (+ 1 y) 2))
(check-sat)

The call was made as follows:

vampire --input_syntax smtlib2 problem.smt2

However, the issue does not occur with problems that are UNSAT.

Also, I was not able to obtain a model, since (get-model) seems not to be supported.

I need to use SMT-LIB2 as an input, because I want to work with Vampire and JavaSMT (github.com/sosy-lab/java-smt) as part of my bachelor thesis.

[MichaelRawson]

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.

[selig]

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.