Mysaa/mpri-2.4-project-2023-2024
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

fix a ConstraintSimplifier bug

Browse Source 
Reported-by: Mathis Bouverot-Dupuis
This commit is contained in:
Gabriel Scherer 2024-02-14 15:57:34 +01:00
parent 1f2bf2bb13
commit fd0213fe82
1 changed files with 1 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/support/ConstraintSimplifier.ml
View File

@ -58,6 +58,7 @@ module Make(T : Utils.Functor) = struct
VarSet.of_list [v1; v2], Eq (v1, v2) VarSet.of_list [v1; v2], Eq (v1, v2)
end end
| Exist (v, s, c) -> | Exist (v, s, c) ->
let v = normalize v in
let fvs, c = simpl (VarSet.add v bvs) c in let fvs, c = simpl (VarSet.add v bvs) c in
if is_in_env v then (fvs, c) if is_in_env v then (fvs, c)
else if not (VarSet.mem v fvs) then (fvs, c) else if not (VarSet.mem v fvs) then (fvs, c)