From 4d02e2a1c7129ce81a01a9ad53e6ef4f4f84eafb Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 12 Aug 2022 23:09:48 -0400 Subject: [PATCH] fix(cc): bug in backtracking --- src/cc/CC.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/cc/CC.ml b/src/cc/CC.ml index 004dec85..0af10dca 100644 --- a/src/cc/CC.ml +++ b/src/cc/CC.ml @@ -218,6 +218,7 @@ let raise_conflict_ (cc : t) ~th (e : Lit.t list) (p : Proof_term.step_id) : _ = Vec.clear cc.combine; Event.emit cc.on_conflict { cc; th; c = e }; Stat.incr cc.count_conflict; + Vec.clear cc.res_acts; raise (E_confl (Conflict (e, p))) let[@inline] all_classes self : repr Iter.t =