From e7124511dc290f61d1469032a7d9f56de018007e Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Tue, 16 Feb 2021 11:12:45 -0800 Subject: [PATCH] [pulse] use only known facts for variable substitutions Summary: Using more than the "known" part of the arithmetic could accidentally leak "pruned" information into certain facts. I noticed this when adding more term equality reasoning to pulse in another diff. At the moment this has little effect but is still more correct conceptually. Reviewed By: ezgicicek Differential Revision: D26450333 fbshipit-source-id: eb31da344 --- infer/src/pulse/PulseFormula.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/infer/src/pulse/PulseFormula.ml b/infer/src/pulse/PulseFormula.ml index b32314118..96ff0a383 100644 --- a/infer/src/pulse/PulseFormula.ml +++ b/infer/src/pulse/PulseFormula.ml @@ -1466,7 +1466,7 @@ end = struct let eliminate_vars ~keep phi = - let subst = VarUF.reorient ~keep phi.both.var_eqs in + let subst = VarUF.reorient ~keep phi.known.var_eqs in try Sat (subst_var subst phi) with Contradiction -> Unsat end @@ -1609,4 +1609,4 @@ let has_no_assumptions phi = Atom.Set.for_all (fun atom -> Formula.Normalizer.implies_atom phi.known atom) phi.pruned -let get_var_repr phi v = (Formula.Normalizer.get_repr phi.both v :> Var.t) +let get_var_repr phi v = (Formula.Normalizer.get_repr phi.known v :> Var.t)