integer optimization bug in python

[amchiclet]

Z3 version 4.8.8.0 Python version 3.8.2

$ pip3 show z3-solver
Name: z3-solver
Version: 4.8.8.0
Summary: an efficient SMT solver library
Home-page: https://github.com/Z3Prover/z3
Author: The Z3 Theorem Prover Project
Author-email: None
License: MIT License
Location: /home/phaosaw2/.local/lib/python3.8/site-packages
Requires:
Required-by:

Here's the code to reproduce the bug.

$ cat maybe-bug.py
from z3 import Int, Optimize, sat

x = Int('x')
constraints = [
    x >= 189,
    x <= 290,
    x + 3 >= 0,
    x + 3 < 999,
    2*x + 3 >= 0,
    2*x + 3 < 999,
    x - 16 >= 0,
    x - 16 < 999,
    2*x - 16 >= 0,
    2*x - 16 < 999,
]

opt = Optimize()
opt.assert_exprs(*constraints)
opt.maximize(x)

if sat == opt.check():
    print('sat')
    print(opt.model().eval(x).as_long())

The code returns 189, when it should be 290.

$ python3 maybe-bug.py
sat
189

Changing the constraint x>=189 to x>=190 gives me 290.

Calling opt.maximize(x) twice gives me 290.

Removing any constraint except the first two, gives me 290.

The rise4fun web interface returns 290 with this code.

(declare-const x Int)
(assert (>= x 189))
(assert (<= x 290))
(assert (>= (+ x 3) 0))
(assert (< (+ x 3) 999))
(assert (>= (+ (* 2 x) 3) 0))
(assert (< (+ (* 2 x) 3) 999))
(assert (>= (- x 16) 0))
(assert (< (- x 16) 999))
(assert (>= (- (* 2 x) 16) 0))
(assert (< (- (* 2 x) 16) 999))
(maximize x)
(check-sat)
(eval x)

Possibly a bug in the Python port.

[rainoftime]

A QF_LRA formula at commit f370d8d9b4f

(set-logic QF_LRA)
(declare-const r0 Real)
(declare-const r1 Real)
(assert (< r0 0.0 r1 0.955441))
(maximize r1)
(check-sat)
(get-objectives)

./z3 smt.arith.solver=6  xx.smt2
sat
(objectives
 (r1 (/ 955441.0 2000000.0))
)

./z3 smt.arith.solver=2 xx.smt2
sat
(objectives
 (r1 (+ (/ 955441.0 1000000.0) (* (- 2.0) epsilon)))
)

Seems a bug in smt.arith.solver=6. Because when I add (assert (> r1 (/ 955441.0 2000000.0))) to the formula, z3 returns sat.

[rainoftime]

For smtlib2 instance by @amchiclet , both smt.arith.solver=6 and smt.arith.solver=2 can return 189 (at commit f370d8d) Perhaps the version in rise4fun is different from 4.8.8.0.

[NikolajBjorner]

Thanks, I know what the bug is (a regression), but don't have a fix right now

[NikolajBjorner]

This is fixed

[rainoftime]

ba5c9c3883, the results of arith.solver=2 and =6 seem different

(set-logic QF_LIA)
(declare-const i2 Int)
(declare-const i4 Int)
(assert (<= (+ (div 214 214) i2) (* i4 61 61)))
(assert (<= (* i4 61 61) (- 76 i2 483 (- 76 214 483) 483) 483))
(minimize (* i4 61 61))
(minimize (+ 61 i2 76))
(minimize 214)
(check-sat)
(get-objectives)

z3 smt.arith.solver=6 xx.smt2
sat
(objectives
 ((* i4 61 61) 0)
 ((+ 61 i2 76)  (interval (- 615) (- 132)))
 (214 214)
)
z3 smt.arith.solver=6 xx.smt2
sat
(objectives
 ((* i4 61 61) 0)
 ((+ 61 i2 76) (- 615))
 (214 214)
)

[Bri2030]

I have version 4.12.2.0 and i have the exact same behavior as described by @amchiclet for the same scenario. Is this an expected behaviour? Thanks.