I have been testing the performance gain to switch to Rust when using the Z3 API. I tested the following use-case, where I build a long formula. Consider the below rust code and the below python code, which both build a z3 formula with 10_000 constants and then call the solver. When running with Rust, I get the following results:

Time to find the model: 0.554883247

When running with Python, actually solving (the call to solver.check()) the model takes 7 times longer

Time to find the model:  4.0679099559783936

I am surprised by this result -- should the Python z3 API not perform a call to low-level binary code when solving the model, and therefore the actual solving should take roughly the same time? What am I missing here?

Rust code:

use z3;
use z3::ast::Ast;
use z3::Solver;
use std::time::Instant;


fn tester() -> () {
    let cfg = z3::Config::new();
    let ctx = z3::Context::new(&cfg);
    let solver = Solver::new(&ctx);

    let x = z3::ast::BV::new_const(&ctx, "x", 32);
    let mut this_formula = Vec::new();
    for i in 0..10000 {
        let y = z3::ast::BV::from_u64(&ctx, i, 32);
        this_formula.push(x._eq(&y));
    }
    let binding = this_formula.iter().map(|x| x).collect::<Vec<_>>();
    let slice = binding.as_slice();
    let formula = z3::ast::Bool::or(&ctx, slice);
    solver.assert(&formula);

    let start = Instant::now();
    let res = solver.check();
    let end = std::time::Instant::now();
    let time_difference = end.duration_since(start);
    let took_time = time_difference.as_secs_f64();
    println!("Time to find the model: {}", took_time);
    if res == z3::SatResult::Sat {
        let model = solver.get_model().unwrap();
        println!("model:");
    }
}

fn main() {
    tester();
}

Python code:

import z3
import time

def tester():
  x = z3.BitVec("x", 32)
  this_formula = []
  for i in range(10000):  # Assuming a loop to make profiling meaningful
      y = z3.BitVecVal(i, 32)
      this_formula.append(x == y)
  formula = z3.Or(this_formula)
  solver = z3.Solver()
  solver.add(formula)
  start_time = time.time()
  res = solver.check()
  end_time = time.time()
  elasped_time = end_time - start_time
  print("Time to find the model: ", elasped_time)
  print("Res", res)

tester()