I'm not sure what you mean by this question. What that lecture covers is essentially how to express an approximation of the operational semantics of a simple la

I'm not sure what you mean by this question. What that lecture covers is essentially how to express an approximation of the operational semantics of a simple language as a logic formula in a very specific kind of logic (ie one of the theories supported by the Z3 SMT solver). It only supports a small number of constructs and data types, and handles infinite loops by placing an arbitrary bound on how far a program can run. It doesn't tell you anything about "all programs" or "all functions".