simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix(smt): perform CC check after theory actions

Browse source
This commit is contained in:
Simon Cruanes 2022-08-20 22:07:21 -04:00
parent e0faf6ba72
commit ca1abd8134
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/smt/solver_internal.ml
View file

@ -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; if not final then CC.assert_lits cc lits;
(* transmit to theories. *) (* transmit to theories. *)
check_cc_with_acts_ self acts; check_cc_with_acts_ self acts;
if final then ( if final then (
Perform_delayed_th.top self acts;
List.iter (fun f -> f self acts lits) self.on_final_check; List.iter (fun f -> f self acts lits) self.on_final_check;
check_cc_with_acts_ self acts; 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 Perform_delayed_th.top self acts
) else ( ) else (
List.iter (fun f -> f self acts lits) self.on_partial_check; 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 Perform_delayed_th.top self acts
); );
() ()