mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
n/a
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
b60f30c802
commit
357a92dfef
|
@ -1451,6 +1451,11 @@ namespace smt {
|
|||
normalize_gain(min_gain.get_rational(), max_gain);
|
||||
}
|
||||
|
||||
if (is_int(x_i) && !max_gain.is_rational()) {
|
||||
max_gain = inf_numeral(floor(max_gain));
|
||||
normalize_gain(min_gain.get_rational(), max_gain);
|
||||
}
|
||||
|
||||
if (!max_inc.is_minus_one()) {
|
||||
if (is_int(x_i)) {
|
||||
TRACE("opt",
|
||||
|
|
Loading…
Reference in a new issue