Symbolic Evaluation for Type Inference in a Dynamic Language
I am not sure you actually understand the terms you use here.

Symbolic execution has nothing to do with type inference

Symbolic execution is used for static analysis of programs, and is a special case of abstract interpretation. The symbolic executor provides an symbolic input value and traces the program execution given that symbolic input value.

Type inference is much simpler: it involves automatically deducing the type of programs. Nowhere is symbolic execution of the program involved.

Type inference is usually undecidable

For a dynamic typed language, type inference is not decidable. Moreover, even we have a static type system, type inference is usually still undecidable.

The only (?) type system we know of that has decidable type inference is the Hindley-Milner type system, i.e. System F with only Rank-1 types (plus a few conservative extensions). It is known that H-M can type imperative programs (such as Standard ML), as long as you can give good typing rules. When I was an undergraduate, we did an exercise in which we implemented H-M type inference for a restricted, strongly-typed version of Scheme (which was imperative). It was a lot of fun, but it also proves that 
type inference is possible for imperative programs.

Update: oh, how could I have left out the canonical reference for polymorphic, inferable typing of imperative programs? The canonical reference would be Xavier Leroy's PhD thesis, Typage polymorphe d'un langage algorithmique (translated into English as Polymorphic typing of an algorithmic language).

I suggest that you start reading on Hindley-Milner and Algorithm W, as a first step (see, e.g., Chapter 22 of Types and Programming Languages by Benjamin C. Pierce). I also suggest that you do more basic reading and learning before asking on CS.SE, as that would make this site work much better. The theory of programming languages is not like coding and must be studied systematically if you want to have a solid grasp of it :-)