From d153c80ca5960ddfb63f38487a29ed3ae44e071f Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 17 Feb 2022 21:21:51 -0500 Subject: [PATCH] details --- src/sat/Solver.ml | 2 ++ src/th-data/Sidekick_th_data.ml | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml index 5e359dc8..54c32636 100644 --- a/src/sat/Solver.ml +++ b/src/sat/Solver.ml @@ -2275,6 +2275,8 @@ module Make(Plugin : PLUGIN) has_no_delayed_actions self && self.next_decisions = [] then ( + (* nothing more to do, that means the plugin is satisfied + with the trail *) raise_notrace E_sat ); (* otherwise, keep on *) diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml index bc3a37f5..1a612f95 100644 --- a/src/th-data/Sidekick_th_data.ml +++ b/src/th-data/Sidekick_th_data.ml @@ -692,7 +692,7 @@ module Make(A : ARG) : S with module A = A = struct match ST_cstors.get self.cstors repr with | None -> None | Some c -> - Log.debugf 20 (fun k->k "(@[th-data.mk-model.find-cstor@ %a@])" Monoid_cstor.pp c); + Log.debugf 5 (fun k->k "(@[th-data.mk-model.find-cstor@ %a@])" Monoid_cstor.pp c); let args = IArray.map (recurse si) c.c_args in let t = A.mk_cstor self.tst c.c_cstor args in Some t