Opt-branch, incorrectly returns "infinity"

[cheshire]

For the following query:

(declare-fun |main::k@2| () Int)
(declare-fun |main::k@3| () Int)
(declare-fun |main::n@3| () Int)
(declare-fun |main::j@2| () Int)
(declare-fun |main::j@3| () Int)
(assert (and
    (<= (* (- 1) |main::k@2|) 0)
    (<= |main::k@2| 1)
    (<= (+ (+ (* (- 1) |main::j@2|) (* (- 1) |main::k@2|)) |main::n@3|) 0)
    (= |main::k@3| (+ (- 1) |main::k@2|))
    (= |main::j@3| (+ 1 |main::j@2|))
))

(maximize (+ (* (- 1) |main::j@3|) (* (- 1) |main::k@3|) |main::n@3|))
(set-option :opt.optsmt_engine basic)
(set-option :opt.priority box)
(check-sat)

I get the bound "oo".

It is obviously incorrect by looking at the query, but it's even more obvious if we ask Z3 itself whether
(= (+ (* (- 1) |main::j@3|) (* (- 1) |main::k@3|) |main::n@3|) 10) (or any number greater than 0 in general) is satisfiable, because the bound should be indeed zero.

What's more interesting, if we drop the constraints 0 <= k@2 <= 1 opt-Z3 correctly returns a bound of 0.

[NikolajBjorner]

fixed by a0f0b53