They can be used for program synthesis. That is, given some high-level specification, you can use an SMT solver to generate code fitting that specification. You can also use them to verify that some code does fit a specification and, if it doesn't, to find the part of the code causing the actual problem (the minimal unsat core).
A particular example would be to take some existing code with holes (just parts left out) and some assertions about the code's behavior, encode both as logic formulas and try to find a satisfying assignment for the holes. When you have a possible assignment, you can verify it with the same encoding. You can then use the satisfying assignment to fill in the holes in the initial program, which are ideally very tedious to code by hand.
A particular example would be to take some existing code with holes (just parts left out) and some assertions about the code's behavior, encode both as logic formulas and try to find a satisfying assignment for the holes. When you have a possible assignment, you can verify it with the same encoding. You can then use the satisfying assignment to fill in the holes in the initial program, which are ideally very tedious to code by hand.