I'm a beginner with z3 and I want use it to solve ILP problems. I've started with a very simple maximization problem like below:
(declare-const x0 Int) (declare-const x1 Int) (declare-const x2 Int) (declare-const x3 Int) (assert (= x0 1)) (assert (= x0 (+ x1 x2))) (assert (= x3 (+ x1 x2))) (maximize (+ (* x0 5) (* x1 10) (* x2 6) (* x3 9) )) (check-sat) (get-objectives) (get-model)
While the maximized solution should be 24, I get +oo:
sat (objectives ((+ (* x0 5) (* x1 10) (* x2 6) (* x3 9)) oo) ) ( (define-fun x2 () Int 0) (define-fun x3 () Int 1) (define-fun x1 () Int 1) (define-fun x0 () Int 1) )
With another even simpler problem, I get the right solution :
(declare-const x Int) (declare-const y Int) (assert (< x 2)) (assert (< (- y x) 1)) (maximize (+ x y)) (check-sat) (get-model) (get-objectives)
sat ( (define-fun x () Int 1) (define-fun y () Int 1) ) (objectives ((+ x y) 2) )
I can't figure out what is the difference ? Thanks your help.