Here is the simplest example using SMT-LIB 2.0 standard supported by many SMT solvers:
(declare-fun a () Int)
(declare-fun b () Int)
(assert (= a b))
(assert (= a 20))
(assert (= b 20))
(check-sat)
You can use http://rise4fun.com/z3 to experiment with it. It will respond "sat" meaning the assertions can be satisfied, meaning then b can be 20.
Then you can replace (assert (= b 20)) with (assert (distinct b 20)). Z3 will respond with "unsat" meaning it's not possible for b to be anything else.