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

fix: more type checks in preprocess

Browse source
This commit is contained in:
Simon Cruanes 2022-09-11 14:26:34 -04:00
parent 3d0461936f
commit 469b97934a
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/preprocess.ml
View file

@ -61,6 +61,7 @@ let preprocess_term_ (self : t) acts (t : term) : term =
(* only accept a box (with possible side effect: new clauses, etc.) *) (* only accept a box (with possible side effect: new clauses, etc.) *)
Log.debugf 20 (fun k -> Log.debugf 20 (fun k ->
k "(@[smt.preprocess.tr@ %a@ :into %a@])" Term.pp t0 Term.pp u); k "(@[smt.preprocess.tr@ %a@ :into %a@])" Term.pp t0 Term.pp u);
assert (Term.(equal (ty t) (ty u)));
u u
| None -> | None ->
(* just preprocess subterms *) (* just preprocess subterms *)
@ -99,6 +100,7 @@ let simplify_and_preproc_lit (self : t) acts (lit : Lit.t) :
k "(@[smt-solver.simplify@ :t %a@ :into %a@])" Term.pp t Term.pp u); k "(@[smt-solver.simplify@ :t %a@ :into %a@])" Term.pp t Term.pp u);
u, Some pr_t_u u, Some pr_t_u
in in
assert (Term.is_bool @@ Term.ty u);
let v = preprocess_term_ self acts u in let v = preprocess_term_ self acts u in
Lit.atom ~sign self.tst v, pr Lit.atom ~sign self.tst v, pr