Skip to content

Commit

Permalink
Find contains edges: remove superfluous constraint
Browse files Browse the repository at this point in the history
Used to ignore predicate occurrences where the predicate
name coincides with a local variable name.
  • Loading branch information
btj committed Dec 6, 2019
1 parent c0e9918 commit 8026c15
Showing 1 changed file with 0 additions and 4 deletions.
4 changes: 0 additions & 4 deletions src/assertions.ml
Expand Up @@ -1205,9 +1205,6 @@ module Assertions(VerifyProgramArgs: VERIFY_PROGRAM_ARGS) = struct
else
[]
| WPredAsn(_, q, true, qtargs, qfns, qpats) ->
begin match try_assoc q#name xs with
Some _ -> []
| None ->
begin match try_assoc q#name predfammap with
Some (_, qtparams, _, qtps, qsymb, _, _) ->
begin match q#inputParamCount with
Expand Down Expand Up @@ -1236,7 +1233,6 @@ module Assertions(VerifyProgramArgs: VERIFY_PROGRAM_ARGS) = struct
end
end
end
end
| WInstPredAsn(l2, target_opt, static_type_name, static_type_finality, family_type_string, instance_pred_name, index, args) ->
let (pmap, qsymb) =
match try_assoc static_type_name classmap1 with
Expand Down

0 comments on commit 8026c15

Please sign in to comment.