Incorrect 'unknown' results after using Z3_solver_translate in multiple threads

[toolCHAINZ]

Hello! I maintain the Rust z3 bindings. Someone (@lixitrixi) recently reported an issue in the rust bindings that I think may be an issue in z3 itself (prove-rs/z3.rs#465).

See below for a minimized version of their Rust snippet:

use z3::{Context, SatResult, Solver, Translate, ast::*};

fn main() {
    let mut handles = Vec::new();

    // Fails for > 12 threads (on my machine)
    for _ in 0..13 {
        handles.push(std::thread::spawn(move || {
            let s = Solver::new();

            let x = Int::fresh_const("x");
            let y = Int::fresh_const("y");

            // Passes without an arbitrary inequality bound on a variable
            s.assert(y.lt(Int::from_i64(2)));

            // Fails with mul, passes with e.g. add
            s.assert(Int::mul(&[&x, &y]).eq(Int::from_i64(-2)));

            let ctx = Context::thread_local();
            let s = s.translate(&ctx);

            // This block should never panic
            assert_eq!(s.check(), SatResult::Sat);
        }));
    }
    for h in handles.into_iter() {
        h.join().unwrap();
    }
}

On my machine, this gives output roughly like the following:

thread '<unnamed>' (99919944) panicked at src/main.rs:24:13:
assertion `left == right` failed
  left: Unknown
 right: Sat
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread 'main' (99919930) panicked at src/main.rs:28:18:
called `Result::unwrap()` on an `Err` value: Any { .. }

The solver.translate() call is wrapping an FFI call to Z3_solver_translate. If I remove the translate call or reduce the number of threads to 8 (the number of logical cores on my CPU), the error goes away. Interestingly, it seems as if it's only reporting unknown in one thread.

As the original issue notes, changing small things about the given assertions (e.g. using addition instead of multiplication) makes this not reproduce. I also tried translating first to a temporary context and translating back into the original context, but this seems to have no effect on it.