Controlling randomness in Z3

Similar (but somewhat opposite) to this SO question, I do want to expose randomness if possible. That is, I want the two consecutive queries to provide different results. Is that possible? Here is my code:

void oren_example()
{
    int i;

    // context + solver
    context ctx;
    solver solver(ctx);

    // sorts
    sort int_sort     = ctx.int_sort();
    sort seq_int_sort = ctx.seq_sort(int_sort);
    sort bool_sort    = ctx.bool_sort();

    // constants
    expr two   = ctx.int_val(2);
    expr five  = ctx.int_val(5);
    expr four  = ctx.int_val(4);
    expr three = ctx.int_val(3);

    // define State sort
    const char *names[4]={"x","A","b","n"};
    sort sorts[4]={int_sort,seq_int_sort,bool_sort,int_sort};
    func_decl_vector projs(ctx);
    sort state_sort = ctx.tuple_sort("State",4,names,sorts,projs).range();

    // define an arbitrary state sigma
    expr sigma = ctx.constant("sigma",state_sort);

    // define some predicate on the state
    func_decl init = function("init",state_sort,bool_sort);
    solver.add(forall(sigma,
        init(sigma) == (
            ((projs[0](sigma))          == two  ) &&
            ((projs[1](sigma).length()) == three) &&
            ((projs[1](sigma).nth(two)) == five ) &&
            ((projs[3](sigma))          == five ))));

    for (int k=0;k<2;k++)
    {
        // create a snapshot
        solver.push();

        // find an initial state
        solver.add(init(sigma));

        // check sat + get model
        if (solver.check() == sat)
        {
            model m = solver.get_model();
            std::cout << "x = " << m.eval(projs[0](sigma)) << "\n";
            std::cout << "A = " << m.eval(projs[1](sigma)) << "\n";
            std::cout << "b = " << m.eval(projs[2](sigma)) << "\n";
            std::cout << "n = " << m.eval(projs[3](sigma)) << "\n";

            int size = m.eval(projs[1](sigma).length()).get_numeral_int();
            std::vector<int> A;
            for (i=0;i<size;i++)
            {
                A.push_back(
                    m.eval(
                        projs[1](sigma).nth(
                            ctx.int_val(i))).get_numeral_int());
            }
            std::cout << "A = { ";
            for (i=0;i<size;i++)
            {
                std::cout << A[i] << " ";
            }
            std::cout << "}\n";
        }

        // restore snapshot
        solver.pop();
    }
}

And the results are the same:

x = 2
A = (seq.++ (seq.unit 6) (seq.unit 7) (seq.unit 5))
b = false
n = 5
A = { 6 7 5 }
x = 2
A = (seq.++ (seq.unit 6) (seq.unit 7) (seq.unit 5))
b = false
n = 5
A = { 6 7 5 } // ideally this would be different than { 6 7 5 } ...