-E smt2:
Seq(RunFirrtlTransformAnnotation(Dependency(SMTLibEmitter)), EmitCircuitAnnotation(SMTLibEmitter.getClass))

override def toString: String = SMTExprSerializer.serialize(this)

override def toString: String = SMTExprSerializer.serialize(this)

private def id(s: String): String = SMTLibSerializer.escapeIdentifier(s)

def encode(sys: TransitionSystem): Iterable[SMTCommand] = {...}

/** Contains code to convert a flat firrtl module into a functional transition system which
  * can then be exported as SMTLib or Btor2 file.
  */

// since this pass only runs on the main module, inlining needs to happen before
  override def optionalPrerequisites: Seq[TransformDependency] = Seq(Dependency[firrtl.passes.InlineInstances])

override protected def execute(state: CircuitState): CircuitState = {
 ...
 // convert the main module
   ...
      case m: ir.Module =>
        new ModuleToTransitionSystem(presetRegs = presetRegs, memInit = memInit, uninterpreted = uninterpreted).run(m)
    }
}

// first pass over the module to convert expressions; discover state and I/O
    m.foreachPort(onPort)
    m.foreachStmt(onStatement)

TransitionSystem(m.name, inputs.toList, states.values.toList, signals.toList, comments.toMap, header)

/** ExtModules annotated as UninterpretedModule will be modelled as
  * UninterpretedFunction (SMTLib) or constant arrays (btor2).
  * This can be useful when trying to abstract over a function that the
  * SMT solver or model checker is struggling with.
  ...
  */

/** checks to see whether the annotation module can actually be abstracted. Use *after* LowerTypes! */
  def checkModule(m: ir.DefModule, anno: UninterpretedModuleAnnotation): Unit = m match {
  ...
  }

val sysInfo = toTransitionSystem(circuit, sysAnnos)

val res = firrtlPhase.transform(
  Seq(
    RunFirrtlTransformAnnotation(Dependency(SMTLibEmitter)),
    new CurrentFirrtlStateAnnotation(Forms.LowForm),
    FirrtlCircuitAnnotation(circuit)
  ) ++: logLevel ++: annos ++: LoweringAnnos ++: opts
)

class FirrtlPhase
    extends PhaseManager(
      targets = Seq(
        Dependency[firrtl.stage.phases.Compiler],
        Dependency[firrtl.stage.phases.ConvertCompilerAnnotations]
      )
    )

override def transform(annotations: AnnotationSeq): AnnotationSeq = {
 ...
 RunFirrtlTransformAnnotation(a.emitter)
}

val sys = res.collectFirst { case TransitionSystemAnnotation(s) => s }.get

case class TransitionSystemAnnotation(sys: TransitionSystem) 

/** Contains code to convert a flat firrtl module into a functional transition system which
  * can then be exported as SMTLib or Btor2 file.
  */
object FirrtlToTransitionSystem extends Transform with DependencyAPIMigration {
}