Test input for https://github.com/Z3Prover/z3/issues/245

Gh245.java

import java.util.Random;
import com.microsoft.z3.*;

public class Gh245
{
    public Gh245() { }

    public static void main(String[] args)
    {        
        int num_threads = 64;
        final Object m_lock = new Object();
        
        for (int i = 0; i < num_threads; i++) {
            Thread thread = new Thread() {
                @Override public void run() {
                    Context ctx = null;
                    
                    synchronized (m_lock) {
                        ctx = new Context();
                    }
                    
                    BoolExpr x = ctx.mkBoolConst("x");
                    BoolExpr y = ctx.mkBoolConst("y");
                    Random rng = new Random();

                    int end = rng.nextInt(20000);
                    for (int j = 0; j < end; j++) {
                        switch (rng.nextInt(4)) {
                        case 0: x = ctx.mkAnd(x, y); break;
                        case 1: y = ctx.mkOr(x, y); break;
                        case 2: x = ctx.mkBoolConst(ctx.mkSymbol(rng.nextInt(256))); break;
                        case 3: y = ctx.mkXor(y, x); break;
                        default: break;
                        }
                    }

                    System.gc();
                    Runtime.getRuntime().runFinalization();
                }
            };

            thread.start();
        }
    }

}