Tableaux SAT solver ignores triggers from Dolmen

[Halbaroth]

While removing the legacy frontend, I ran our non regression test suite with the SAT solver Tableaux. I caught a bug. This test failed:

(set-logic ALL)
(declare-fun P (Int) Bool)
(declare-fun f (Int) Int)

; This quantifier is explicitly annotated with a (f x) trigger.
; It should not cause this problem to be unsat.
(assert
 (forall ((x Int))
  (! (not (P x)) :pattern ((f x)))))

; Note that we don't use (f 0).
(assert (P 0))

(check-sat)

We got unsat even if we should not because the trigger prevents us from instantiating the axiom. It seems that the fix in #1051 have not been tested with Tableaux.

Notice that the bug affects Tableaux-CDCL too.

[bclement-ocp]

I don't think this is related to Dolmen -- this file is also proved by the legacy frontend. This seems to be due to the Backward instantiation pass which seems to always compute triggers (ignoring matching) and instantiate all lemmas that can prove things from (P e1 .. en) whenever (P e1 .. en) is in the context.