Skip to content

Commit

Permalink
Apply suggestions from code review
Browse files Browse the repository at this point in the history
Co-authored-by: Pierrot <tiky.halbaroth@gmail.com>
  • Loading branch information
bclement-ocp and Halbaroth authored Oct 4, 2023
1 parent 9cf69f1 commit 59ca921
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/lib/reasoners/theory.ml
Original file line number Diff line number Diff line change
Expand Up @@ -394,12 +394,12 @@ module Main_Default : S = struct
()
| Pinfinity | Minfinity ->
(* We should block case-split at infinite values.
Otherwise. Otherwise, we may have soundness issues. We
Otherwise, we may have soundness issues. We
may think an objective is unbounded, but some late
constraints may make it bounded.
An alternative is to only allow further splits when we
know that no extra-assumpptions will be propagated to
know that no extra assumptions will be propagated to
the env. Hence the test 'if for_model' *)
if for_model then ()
else
Expand Down

0 comments on commit 59ca921

Please sign in to comment.