From 59ca9213fb952706d6deba9cafb440383ee13069 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= <129742207+bclement-ocp@users.noreply.github.com> Date: Wed, 4 Oct 2023 18:10:59 +0200 Subject: [PATCH] Apply suggestions from code review Co-authored-by: Pierrot --- src/lib/reasoners/theory.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml index 34acde8ef7..fe10fc1526 100644 --- a/src/lib/reasoners/theory.ml +++ b/src/lib/reasoners/theory.ml @@ -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