search

OCamlPro / alt-ergo

OCamlPro public development repository for Alt-Ergo
https://alt-ergo.ocamlpro.com/
Other
132 stars 33 forks source link

`Tableaux` SAT solver ignores triggers from Dolmen #1242

Open Halbaroth opened 1 month ago

Halbaroth commented 1 month ago

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 commented 1 month ago

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.