z3
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)
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.