Rust Quickstart

Given the following main.rs file:

use owi_sym::Symbolic;

fn mean_wrong(x: i32, y: i32) -> i32 {
    (x + y) / 2
}

fn mean_correct(x: i32, y: i32) -> i32 {
    (x & y) + ((x ^ y) >> 1)
}

fn main() {
    let x = i32::symbol();
    let y = i32::symbol();
    owi_sym::assert(mean_wrong(x, y) == mean_correct(x, y))
}

Let's check if the two functions are the same for any input:

$ owi rust ./mean.rs -w1 --fail-on-assertion-only --no-assert-failure-expression-printing --deterministic-result-order
owi: [ERROR] Assert failure
model {
  symbol symbol_0 i32 -487586839
  symbol symbol_1 i32 486539486
}
owi: [ERROR] Reached problem!
[13]

Indeed, in this case, there will be an integer overflow in one of the two functions and thus they won't give the same result.