Using SMT Solvers in formula checking
Yes, absolutely. SMT solvers are actually quite well suited for such problems. Unfortunately, the input language to them (SMTLib) is rather machine-oriented, but there are many "high-level" interfaces to many solvers, Z3 itself providing a Python interface, for instance.

For this problem, I'll use the Haskell SBV library, which translates your constraints more or less directly to Z3. Note that I've put the equations into SSA form (single-static assignment), as is usual in such analyses. The whole problem is:

{-# LANGUAGE ScopedTypeVariables #-}

import Data.SBV

q = do k1 &lt;- sInt32 "k1"
       k2 &lt;- sInt32 "k2"

       a0 :: SInt32 &lt;- forall "a"
       b0 :: SInt32 &lt;- forall "b"
       c0 :: SInt32 &lt;- forall "c"
       d0 :: SInt32 &lt;- forall "d"

       let a1 = b0 + 1
           c1 = d0
           c2 = c1 `xor` d0
           a2 = a1 + c2
           a3 = a2 + 4

       constrain $ a3 .== b0 + k1
       constrain $ a3 .== d0 + k2


Also note that I (arbitrarily) picked 32-bit integers, though you can go with other types as well as needed. As stated, we get:

*Main&gt; sat q
Unsatisfiable


Meaning that there's no such k1/k2 that satisfy your equations, as you yourself observed. If we let go of the second constraint (by commenting out the very last line in the definition of q), we get:

*Main&gt; sat q
Satisfiable. Model:
  k1 = 5 :: Int32
  k2 = 0 :: Int32


Here's the solver picked the arbitrary value of 0 for k2 since there are no constraints on it; but k1 became 5 as you predicted.

Long story short, yes; this sort of reasoning is absolutely possible with SMT-solvers; and there are high-level language bindings that let you express them rather concisely.