Symbolic reachability analysis using rewriting with Satisfiability Modulo Theories (SMT) has been used to model different systems, including a variety of security protocols. Recently, it has also been used to analyze Parametric Timed Automata (PTAs). These techniques are based on reachability in a finite state graph generated from concrete initial states where each generated state is constrained by a SMT expression checked for satisfiability. In this work, we propose to generate a finite state graph not by rewriting with SMT but by narrowing with SMT. Narrowing with SMT allows a greater generalization, since (i) an infinite number of initial states can be represented by a finite number of states with variables, not only SMT variables, and (ii) an infinite state graph from a concrete initial state may be represented by a finite state graph from an initial state with variables. We use graph search pruning techniques via irreducible terms and SMT constraints on conditional rules. This is supported by a novel folding SMT narrowing technique to represent infinite computations in a finite way. Additionally, we present a new textual user interface that allows the use of the algorithm in a simpler and more readable way.