(set-option :verbose true) (declare-const x Real) (assert (= (+ (* 2.0 x) -2.0 2.0 (* -1.0 x)) 1.0)) (debug graph) (check-sat) (get-model) ------------------------- 0 ==> true 1 ==> false 2 ==> x 3 ==> 1.0 4 ==> $2 = $3 5 ==> assert $4 sat 2 iterations of propagation 0 decisions 6 narrowing of a value interval 6 narrowing of a constraint interval x = 1.0