SMTLIB declaration dependencies ignored

[FedericoAureliano]

Sometimes we declare types in the incorrect order, leading SMT solvers to fail. For example,

module main {
    type t;
    datatype a = A(x: t);

    var y: a;
    var z: t;

    init {
        assert y.x == z;
    }

    control {
        bmc(0);
        check;
        print_results;
    }
}

leads to a being declared before t using the SMTLIB interface.