Bad performance on simple long query

[kfriedberger]

We have found a simple and long SMT query (smt_278.zip) where SMTInterpol needs more time than expected.

What would one 'expect' from SMT solving, which is by definition a computationally hard problem? :-) Well, SMTInterpol required about 40s for the query, several other SMT solvers require less than 5s. Overall, SMTInterpol is not doing bad, but it could do better in some cases. :-)

Perhaps the SMTInterpol team could look for solving such a query faster?

The SMT query (smt_278.zip) has 4000 variables of type Bool or Int. The structure is a large conjunction with many small formulas.