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 1 year 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