z3 icon indicating copy to clipboard operation
z3 copied to clipboard

4.8.5 and 4.13.0 hang on example that works in 4.6.0 (linear constraints with int variables)

Open sm178 opened this issue 10 months ago • 0 comments

I have this relatively simple problem where Z3 in versions 4.8.5 and 4.13.0 (2 I tested) seems to hang indefinitely:

(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun e () Int)
(declare-fun f () Int)
(assert (and
     (<= 0 f)
     (<= f 10)
     (<= 0 e)
     (<= e 10)
     (<= 0 d)
     (<= d 10)
     (<= 0 c)
     (<= c 10)
     (<= 0 b)
     (<= b 10)
     (<= 0 a)
     (<= a 10)))
(assert (<= (+ a b c d e f) 25))
(assert (<= (+ a b c (- d) (- e) (- f)) 1000))
(assert (<= (- 1000) (+ a b c (- d) (- e) (- f))))
(minimize (* (- 1) (+ a b c d e f)))
(check-sat)

On the other hand 4.6.0 gives the answer immediately. Not sure if I'm doing something wrong, or if it's a problem with Z3 itself. If I remove one of the constraints, (assert (<= (+ a b c d e f) 25)), both the old and new version return immediately.

sm178 avatar Apr 10 '24 07:04 sm178