let strong_depends solver p q =
  Depsolver_int.S.reset solver.Depsolver_int.constraints;
  let solver = Depsolver_int.copy_solver solver in
  let lit = Depsolver_int.S.lit_of_var (solver.Depsolver_int.map#vartoint q) false in
  Depsolver_int.S.add_rule solver.Depsolver_int.constraints [|lit|] [];
  match Depsolver_int.solve solver (Diagnostic_int.Sng p) with
  |Depsolver_int.Failure _ -> true
  |Depsolver_int.Success _ -> false