1
Vote

bounds seem to be ignored

description

When I run the following small program, I get sat, despite the fact that bounds +-2 were added via add-bounds. It looks as if the bounds were ignored.

Input:

;;;
;;; add-bounds.smt2
;;;
;;; execute with z3 -smt2 add-bounds.smt2 >add-bounds.txt
;;;

;; define a simple CSP with 2 variables
(declare-const x Real)
(declare-const y Real)

(assert (or (< x 0) (< 0 x)))
(assert (or (< y 0) (< 0 y)))
(assert (and (= y (* 3 x)) (= y (+ x 6))))

(check-sat)
(get-model)

(apply add-bounds)

(check-sat)

(get-model)

Output:

sat
(model
(define-fun y () Real
9.0)
(define-fun x () Real
3.0)
)
(goals
(goal
(or (< x (to_real 0)) (< (to_real 0) x))
(or (< y (to_real 0)) (< (to_real 0) y))
(= y (* (to_real 3) x))
(= y (+ x (to_real 6)))
(<= x 2.0)
(>= x (- 2.0))
(<= y 2.0)
(>= y (- 2.0))
:precision under :depth 1)
)
sat
(model
(define-fun y () Real
9.0)
(define-fun x () Real
3.0)
)

file attachments

comments

wintersteiger wrote Mar 1, 2016 at 1:28 PM

This issue tracker is not in use anymore as Z3 has moved to GitHub. Please submit a new issue in our new issue tracker.