Unexpected performance problem

[okigan]

Hello and thank you for wonderful tool!

I ran into performance issue on seemingly simple problem.

Using latest z3py 4.12.1.0, which I tried locally and google colab - check() method does not return/hangs. It does work with 3 variables, slower with 4, and with 5 it hangs.

Please advise how to give enough hints/option to let it converge to solution.

Here is sexpr for it:

(declare-fun d () Int)
(declare-fun c () Int)
(declare-fun b () Int)
(declare-fun a () Int)
(assert (and (>= a 0) (>= b 0) (>= c 0) (>= d 0) (>= e 0)))
(assert (and (<= a 100) (<= b 100) (<= c 100) (<= d 100) (<= e 100)))
(assert (<= (+ a b c d e) 100))
(minimize (+ (ite (> (- 0 a) 0) (- 0 a) (- (- 0 a)))
   (ite (> (- 16 b) 0) (- 16 b) (- (- 16 b)))
   (ite (> (- 33 c) 0) (- 33 c) (- (- 33 c)))
   (ite (> (- 50 d) 0) (- 50 d) (- (- 50 d)))
   (ite (> (- 66 e) 0) (- 66 e) (- (- 66 e)))))
(check-sat)```


In the minimize clause I've tried to replace the Abs() with squaring the value, but that did not improve things.

[nunoplopes]

Try using bit-vectors. Might be faster.