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

details

Browse source
This commit is contained in:
Simon Cruanes 2021-12-17 13:46:48 -05:00
parent 46b13d08d0
commit f9f471ce12
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 2 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -321,12 +321,12 @@ module Make(A : ARG) : S with module A = A = struct
let (module Act) = acts in let (module Act) = acts in
let u = let u =
let args = let sel_args =
A.Cstor.ty_args cstor A.Cstor.ty_args cstor
|> Iter.mapi (fun i ty -> A.mk_sel self.tst cstor i t) |> Iter.mapi (fun i ty -> A.mk_sel self.tst cstor i t)
|> Iter.to_array |> IArray.of_array_unsafe |> Iter.to_array |> IArray.of_array_unsafe
in in
A.mk_cstor self.tst cstor args A.mk_cstor self.tst cstor sel_args
in in
(* proof: resolve [is-c(t) |- t = c(sel-c-0(t), …, sel-c-n(t))] (* proof: resolve [is-c(t) |- t = c(sel-c-0(t), …, sel-c-n(t))]
@ -346,7 +346,6 @@ module Make(A : ARG) : S with module A = A = struct
T.Tbl.add self.case_split_done t (); (* no need to decide *) T.Tbl.add self.case_split_done t (); (* no need to decide *)
Act.add_clause [Act.mk_lit_nopreproc (A.mk_eq self.tst t u)] proof; Act.add_clause [Act.mk_lit_nopreproc (A.mk_eq self.tst t u)] proof;
None None
| _ -> None | _ -> None