fix(term): hashconsing error leading to non termination

src/base-term/Base_types.ml

@@ -549,6 +549,8 @@ end = struct
         Fun.equal f1 f2 && IArray.equal sub_eq a1 a2
       | Eq(a1,b1), Eq(a2,b2) -> sub_eq a1 a2 && sub_eq b1 b2
       | Not a, Not b -> sub_eq a b
+      | Ite (a1,b1,c1), Ite (a2,b2,c2) ->
+        sub_eq a1 a2 && sub_eq b1 b2 && sub_eq c1 c2
       | (Bool _ | App_fun _ | Eq _ | Not _ | Ite _), _
         -> false
 

src/msat-solver/Sidekick_msat_solver.ml

@@ -558,6 +558,7 @@ module Make(A : ARG)
 
   let add_clause (self:t) (c:Atom.t IArray.t) : unit =
     Stat.incr self.count_clause;
+    Log.debugf 50 (fun k->k "add clause %a@." (Util.pp_iarray Atom.pp) c);
     Sat_solver.add_clause_a self.solver (c:> Atom.t array) P.default
 
   let add_clause_l self c = add_clause self (IArray.of_list c)

src/smtlib/Process.ml

@@ -200,7 +200,7 @@ let process_stmt
     (solver:Solver.t)
     (stmt:Statement.t) : unit or_error =
   Log.debugf 5
-    (fun k->k "(@[<2>process statement@ %a@])" Statement.pp stmt);
+    (fun k->k "(@[smtlib.process-statement@ %a@])" Statement.pp stmt);
   let decl_sort c n : unit =
     Log.debugf 1 (fun k->k "(@[declare-sort %a@ :arity %d@])" ID.pp c n);
     (* TODO: more? *)