I've done some exploration of this using SyGuS and quantified SMT. See for example http://svn.clifford.at/handicraft/2018/xbitpermsyn/ …. (Also submitted some SyGuS benchmarks.) A big unsolved problem seems to be generating programs that contain large (word-sized) magic constants.
-
This Tweet is unavailable.
-
This Tweet is unavailable.
-
This Tweet is unavailable.
-
This Tweet is unavailable.
-
This Tweet is unavailable.
-
This Tweet is unavailable.
-
I think it's one of those things that are obvious once you have more experience with smt solvers, but at the same time the whole field is too young for any of that to be "textbook knowledge". I had a few similar (in spirit) gotchas with writing sat encodings.
But maybe in a few years all of that will be handled inside of exist-forall engines and most users will not need to care what is happening "under the hood". 
