diff options
| author | Son Ho | 2022-01-27 00:11:59 +0100 |
|---|---|---|
| committer | Son Ho | 2022-01-27 00:11:59 +0100 |
| commit | 1e3e6f6ecdbc277322f3631dac683fe938134d0c (patch) | |
| tree | 1206907aa89d96b3dc762063ecbf715540d08b3e /src | |
| parent | bf11d4d993b3dce15ae61bb54caac4bae1bbe27a (diff) | |
Cleanup a bit
Diffstat (limited to 'src')
| -rw-r--r-- | src/Invariants.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/src/Invariants.ml b/src/Invariants.ml index b61763ff..522f2ffa 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -601,7 +601,6 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = (* Also check that the symbolic values contain regions of interest - * otherwise they should have been reduced to `_` *) let abs = Option.get info in - log#ldebug (lazy (symbolic_value_to_string ctx sv)); assert (ty_has_regions_in_set abs.regions sv.V.sv_ty) | V.AProjBorrows (sv, proj_ty) -> let ty2 = Subst.erase_regions sv.V.sv_ty in @@ -609,7 +608,6 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = (* Also check that the symbolic values contain regions of interest - * otherwise they should have been reduced to `_` *) let abs = Option.get info in - log#ldebug (lazy (symbolic_value_to_string ctx sv)); assert (ty_has_regions_in_set abs.regions proj_ty) | V.AEndedProjLoans (_msv, given_back_ls) -> List.iter |