(set-option :verbose true) (declare-const x Real) (declare-const y Real) (assert (= (+ x y) 5.0)) (debug graph) (check-sat) (get-model) ------------------------- 0 ==> true 1 ==> false 2 ==> x 3 ==> y 4 ==> $2 + $3 5 ==> 5.0 6 ==> $4 = $5 7 ==> assert $6 delta_sat with absolute precision 0.0009765625 25 iterations of propagation 12 decisions 51 narrowing of a value interval 30 narrowing of a constraint interval x = [-0.000000,0.000977] y = [4.999023,5.000000]