Wrong encoding of signed divisions

[fpoli]

Given a / b, for a < 0 in Rust the result is still rounded toward 0, while in Viper it is rounded away from 0. Prusti currently encodes signed integer divisions using Viper's semantics, which is wrong.

use prusti_contracts::*;

// To inhibit constant-propagation optimizations:
#[pure]
fn id<T>(x: T) -> T { x}

pub fn main(){
    assert!(id(3i32) / 2 == 1);
    assert!(id(-3i32) / 2 == -1);
    assert!(id(3i32) / -2 == -1);
    assert!(id(-3i32) / -2 == 1);
    prusti_assert!(id(3i32) / 2 == 1);
    prusti_assert!(id(-3i32) / 2 == -1);
    prusti_assert!(id(3i32) / -2 == -1);
    prusti_assert!(id(-3i32) / -2 == 1);
    assert!(false); // Smoke test, the only one that should fail
}

If someone wants to work on this, the fix can be done similarly to how fn rem is used to encode the correct semantics of signed modulo operations.

[fpoli]

It might be better to add something like -Z mir-opt-level=0 to all our test cases. I'm afraid that many useful tests might have been invalidated by the experimental MIR-level optimizations that are enabled by default in nighly compiler versions.

[fpoli]

Silver has the same issue: https://github.com/viperproject/silver/issues/782