(set-option :verbose true) (declare-const x Real) (assert (= (ln x) 1.0)) (debug graph) (check-sat) (get-model) ------------------------- 0 ==> true 1 ==> false 2 ==> x 3 ==> (ln $2) 4 ==> 1.0 5 ==> $3 = $4 6 ==> assert $5 delta_sat with absolute precision 0.0000000000000002220446049250313 2 iterations of propagation 0 decisions 7 narrowing of a value interval 7 narrowing of a constraint interval x = [2.718281,2.718282]