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 debug msg

Browse source
This commit is contained in:
Simon Cruanes 2022-09-16 19:49:58 -04:00
parent 0b951b92d3
commit c49edd8d70
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/smt/th_combination.ml
View file

@ -25,7 +25,7 @@ let processed_ (self : t) t : bool =
| Some set -> T.Set.mem t set | Some set -> T.Set.mem t set
let add_term_needing_combination (self : t) (t : T.t) : unit = let add_term_needing_combination (self : t) (t : T.t) : unit =
if not (processed_ self t) && not (T.is_bool @@ T.ty t) then ( if (not (processed_ self t)) && not (T.is_bool @@ T.ty t) then (
Log.debugf 50 (fun k -> k "(@[th.comb.add-term-needing-comb@ %a@])" T.pp t); Log.debugf 50 (fun k -> k "(@[th.comb.add-term-needing-comb@ %a@])" T.pp t);
Vec.push self.unprocessed t Vec.push self.unprocessed t
) )
@ -42,7 +42,8 @@ let pop_new_lits (self : t) : Lit.t list =
in in
if not (T.Set.mem t set_for_ty) then ( if not (T.Set.mem t set_for_ty) then (
Stat.incr self.n_terms; Stat.incr self.n_terms;
Log.debugf 0 (fun k -> k "NEED TH COMBINATION %a" T.pp t); Log.debugf 10 (fun k ->
k "(@[th-comb.term.need-th-combination@ %a@])" T.pp t);
(* now create [t=u] for each [u] in [set_for_ty], and add it to [lits] *) (* now create [t=u] for each [u] in [set_for_ty], and add it to [lits] *)
T.Set.iter T.Set.iter