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(preprocess): type check was invalid

Browse source
This commit is contained in:
Simon Cruanes 2022-09-11 14:50:18 -04:00
parent c18b824037
commit 2764882f50
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/preprocess.ml
View file

@ -61,7 +61,7 @@ let preprocess_term_ (self : t) acts (t : term) : term =
(* only accept a box (with possible side effect: new clauses, etc.) *)
Log.debugf 20 (fun k ->
k "(@[smt.preprocess.tr@ %a@ :into %a@])" Term.pp t0 Term.pp u);
assert (Term.(equal (ty t) (ty u)));
assert (Term.(equal (ty t0) (ty u)));
u
| None ->
(* just preprocess subterms *)