From 2922cca78f8e3854c77f9fd828f8090c8d6a0647 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Fri, 22 Jul 2022 21:54:22 -0400
Subject: [PATCH] fix: proper negation when raising an acyclicity conflict

---
 src/th-data/Sidekick_th_data.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml
index bcf2b0b6..1c02d6be 100644
--- a/src/th-data/Sidekick_th_data.ml
+++ b/src/th-data/Sidekick_th_data.ml
@@ -630,7 +630,9 @@ module Make (A : ARG) : S with module A = A = struct
               k "(@[%s.acyclicity.raise_confl@ %a@ @[:path %a@]@])" name Expl.pp
                 expl pp_path path);
           let lits, pr = SI.cc_resolve_expl solver expl in
-          SI.raise_conflict solver acts lits pr
+          (* negate lits *)
+          let c = List.rev_map SI.Lit.neg lits in
+          SI.raise_conflict solver acts c pr
         | { flag = New; _ } as node_r ->
           node_r.flag <- Open;
           let path = (n, node_r) :: path in