simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-10 21:24:06 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

details

Browse source
This commit is contained in:
Simon Cruanes 2022-02-17 21:21:51 -05:00
parent 8530c07c59
commit d153c80ca5
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
2 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/sat/Solver.ml
View file

@ -2275,6 +2275,8 @@ module Make(Plugin : PLUGIN)
has_no_delayed_actions self && has_no_delayed_actions self &&
self.next_decisions = [] self.next_decisions = []
then ( then (
(* nothing more to do, that means the plugin is satisfied
with the trail *)
raise_notrace E_sat raise_notrace E_sat
); );
(* otherwise, keep on *) (* otherwise, keep on *)

2
src/th-data/Sidekick_th_data.ml
View file

@ -692,7 +692,7 @@ module Make(A : ARG) : S with module A = A = struct
match ST_cstors.get self.cstors repr with match ST_cstors.get self.cstors repr with
| None -> None | None -> None
| Some c -> | 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 args = IArray.map (recurse si) c.c_args in
let t = A.mk_cstor self.tst c.c_cstor args in let t = A.mk_cstor self.tst c.c_cstor args in
Some t Some t