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

details

Browse source
This commit is contained in:
Simon Cruanes 2022-08-22 22:09:58 -04:00
parent dde63a9ef2
commit 6ad07921c4
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
2 changed files with 4 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/smt/solver_internal.ml
View file

@ -314,17 +314,17 @@ let cc_resolve_expl self e : lit list * _ =
(** {2 Interface with the SAT solver} *) (** {2 Interface with the SAT solver} *)
let rec push_lvl_ = function let rec push_lvl_theories_ = function
| Ths_nil -> () | Ths_nil -> ()
| Ths_cons r -> | Ths_cons r ->
r.push_level r.st; r.push_level r.st;
push_lvl_ r.next push_lvl_theories_ r.next
let rec pop_lvls_ n = function let rec pop_lvls_theories_ n = function
| Ths_nil -> () | Ths_nil -> ()
| Ths_cons r -> | Ths_cons r ->
r.pop_levels r.st n; r.pop_levels r.st n;
pop_lvls_ n r.next pop_lvls_theories_ n r.next
(** {2 Model construction and theory combination} *) (** {2 Model construction and theory combination} *)

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

@ -715,7 +715,6 @@ end = struct
) )
let on_partial_check self solver acts trail = let on_partial_check self solver acts trail =
Profile.with_ "data.partial-check" @@ fun () ->
check_is_a self solver acts trail; check_is_a self solver acts trail;
() ()