Skip to content

Commit

Permalink
revert part #11126 (#11347)
Browse files Browse the repository at this point in the history
We need to raise invalid arg because that is what we're catching  in:

```
            (* If [user_var] is selected, don't select an incompatible version of
               the optional dependency. We don't need to do this explicitly in
               the [essential] case, because we must select a good version and we can't
               select two. *)
            (try S.at_most_one sat (user_var :: fail) |> ignore with
             | Invalid_argument reason ->
               (* Explicitly conflicts with itself! *)
               S.at_least_one sat [ S.neg user_var ] ~reason)
```

Signed-off-by: Rudi Grinberg <[email protected]>
  • Loading branch information
rgrinberg authored Jan 19, 2025
1 parent e5030ca commit 8e544a5
Showing 1 changed file with 5 additions and 4 deletions.
9 changes: 5 additions & 4 deletions src/sat/sat.ml
Original file line number Diff line number Diff line change
Expand Up @@ -624,10 +624,11 @@ module Make (User : USER) = struct

(* Ensure no duplicates *)
if List.length (remove_duplicates lits) <> List.length lits
then
User_error.raise
[ Pp.text "at_most_one(" ++ pp_lits lits ++ Pp.paragraph "): duplicates in list!"
];
then (
let msg =
Pp.text "at_most_one(" ++ pp_lits lits ++ Pp.paragraph "): duplicates in list!"
in
invalid_arg (Format.asprintf "%a." Pp.to_fmt msg));
(* Ignore any literals already known to be False.
If any are True then they're enqueued and we'll process them
soon. *)
Expand Down

0 comments on commit 8e544a5

Please sign in to comment.