From ca1abd81345439b6ba9333f920a025c731ccb497 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 20 Aug 2022 22:07:21 -0400 Subject: [PATCH] fix(smt): perform CC check after theory actions --- src/smt/solver_internal.ml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/smt/solver_internal.ml b/src/smt/solver_internal.ml index 08d51ad3..be2b369d 100644 --- a/src/smt/solver_internal.ml +++ b/src/smt/solver_internal.ml @@ -489,7 +489,10 @@ let assert_lits_ ~final (self : t) (acts : theory_actions) (lits : Lit.t Iter.t) if not final then CC.assert_lits cc lits; (* transmit to theories. *) check_cc_with_acts_ self acts; + if final then ( + Perform_delayed_th.top self acts; + List.iter (fun f -> f self acts lits) self.on_final_check; check_cc_with_acts_ self acts; @@ -536,6 +539,8 @@ let assert_lits_ ~final (self : t) (acts : theory_actions) (lits : Lit.t Iter.t) Perform_delayed_th.top self acts ) else ( List.iter (fun f -> f self acts lits) self.on_partial_check; + (* re-check CC after theory actions, which might have merged classes *) + check_cc_with_acts_ self acts; Perform_delayed_th.top self acts ); ()