From 721b1874b7ba0b6d16460bf2c84261867a38d685 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Fri, 1 Nov 2019 16:07:05 -0500
Subject: [PATCH] fix: re-check CC after calling `on-final-check`

---
 src/msat-solver/Sidekick_msat_solver.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml
index b625c4ea..fc3de178 100644
--- a/src/msat-solver/Sidekick_msat_solver.ml
+++ b/src/msat-solver/Sidekick_msat_solver.ml
@@ -310,6 +310,8 @@ module Make(A : ARG)
       CC.check cc acts;
       if final then (
         List.iter (fun f -> f self acts lits) self.on_final_check;
+        CC.check cc acts;
+        (* TODO: theory combination until fixpoint *)
       ) else (
         List.iter (fun f -> f self acts lits) self.on_partial_check;
       );