From d11b9d585cf6f13766094c9574325f23f8d16659 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Fri, 4 Feb 2022 16:40:55 -0500
Subject: [PATCH] fix(smt): improve theory combination a bit

---
 src/lra/sidekick_arith_lra.ml         |  1 -
 src/smt-solver/Sidekick_smt_solver.ml | 27 +++++++++++++++------------
 2 files changed, 15 insertions(+), 13 deletions(-)

diff --git a/src/lra/sidekick_arith_lra.ml b/src/lra/sidekick_arith_lra.ml
index bac4dcf4..34949acb 100644
--- a/src/lra/sidekick_arith_lra.ml
+++ b/src/lra/sidekick_arith_lra.ml
@@ -363,7 +363,6 @@ module Make(A : ARG) : S with module A = A = struct
       end
 
     | LRA_op _ | LRA_mult _ ->
-      let steps = ref [] in
       let le = as_linexp t in
 
       (* [t] is [le_comb + le_const], where [le_comb] is a linear expression
diff --git a/src/smt-solver/Sidekick_smt_solver.ml b/src/smt-solver/Sidekick_smt_solver.ml
index 2db21dc1..ee47ba55 100644
--- a/src/smt-solver/Sidekick_smt_solver.ml
+++ b/src/smt-solver/Sidekick_smt_solver.ml
@@ -304,6 +304,7 @@ module Make(A : ARG)
     let[@inline] ty_st t = t.ty_st
     let[@inline] proof self = self.proof
     let stats t = t.stat
+    let[@inline] has_delayed_actions self = not (Queue.is_empty self.delayed_actions)
 
     let registry self = self.registry
     let simplifier self = self.simp
@@ -543,8 +544,6 @@ module Make(A : ARG)
       CC.pop_levels (cc self) n;
       pop_lvls_ n self.th_states
 
-    exception E_loop_exit
-
     (* handle a literal assumed by the SAT solver *)
     let assert_lits_ ~final (self:t) (acts:theory_actions) (lits:Lit.t Iter.t) : unit =
       Log.debugf 2
@@ -558,19 +557,23 @@ module Make(A : ARG)
       (* transmit to theories. *)
       CC.check cc acts;
       if final then (
-        try
-          while true do
+        let continue = ref true in
+        while !continue do
+          let fcheck = ref true in
+          while !fcheck do
             (* TODO: theory combination *)
             List.iter (fun f -> f self acts lits) self.on_final_check;
-            Perform_delayed_th.top self acts;
-            CC.check cc acts;
-            Perform_delayed_th.top self acts;
-            if not @@ CC.new_merges cc then (
-              raise_notrace E_loop_exit
-            );
+            if has_delayed_actions self then (
+              Perform_delayed_th.top self acts;
+            ) else (
+              fcheck := false
+            )
           done;
-        with E_loop_exit ->
-          ()
+          CC.check cc acts;
+          if not (CC.new_merges cc) && not (has_delayed_actions self) then (
+            continue := false;
+          );
+        done;
       ) else (
         List.iter (fun f -> f self acts lits) self.on_partial_check;
         Perform_delayed_th.top self acts;