From 3124d55209a049d7520228e97d3da27b42f2fa81 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Tue, 22 Nov 2016 17:04:18 +0100 Subject: [PATCH] [bugfix?] Avoid forgetting theory conflict clauses When theory raises a conflict, it is analysed, and the backtracck clause that result is added to the solver, however, I didn't find yet a satisfying answer as to wether the original clause is implied (or not) by this backtrack clause, so in order not to lose information, we also add the original conflict clause when it comes from the theory (because if not, then it comes from a conflict detected during propgation, so the conflict clause is actually already attached). --- src/core/internal.ml | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/core/internal.ml b/src/core/internal.ml index c4e50bad..fddca67e 100644 --- a/src/core/internal.ml +++ b/src/core/internal.ml @@ -1006,7 +1006,14 @@ module Make match propagate () with | Some confl -> (* Conflict *) incr conflictC; - add_boolean_conflict confl + (* When the theory has raised Unsat, add_boolean_conflict + might 'forget' the initial conflict clause, and only add the + analyzed backtrack clause. So in those case, we use add_clause + to make sure the initial conflict clause is also added. *) + if confl.attached then + add_boolean_conflict confl + else + add_clause confl | None -> (* No Conflict *) assert (env.elt_head = Vec.size env.elt_queue);