"Sorts (_ BitVec 128) and Int are incompatible"

[yihuang]

I tried to run MIRAI on one of our crate, but I got this error message:

Error: Sorts (_ BitVec 128) and Int are incompatible
error: could not compile `chain-core`.

To learn more, run the command again with --verbose.

I follow the doc to install recent MIRAI, runs something like this:

$ export RUSTFLAGS="-Z always_encode_mir"
$ cargo build -p chain-core
$ touch $CRATE/src/lib.rs
$ RUSTC_WRAPPER=mirai cargo build -p chain-core

[hermanventer]

I am sorry, but you've run into a bug in MIRAI itself. It encoded a query for the Z3 theorem prover that does not satisfy the typing requirements of Z3. Unfortunately, the way Z3 communicates its displeasure is by throwing a C++ exception that terminates the MIRAI process.

You can work around this by using "MIRAI_LOG=info" to determine which function is being analyzed when this bug occurs. If you then replace the function body with an abstract summary, the analyses may get a bit further.

It would also be great if you can provide me with a code snippet that reproduces this bug, so that I can fix it promptly.

Thanks for trying out MIRAI and giving feedback.

[yihuang]

Thanks for your reply, this is the minimal code that reproduces the issue:

use fixed::types::I65F63 as Fixed;

pub fn test(x: Fixed) -> Fixed {
    x * x
}

With dependencies:

[dependencies]
fixed = "0.5.6"

[hermanventer]

Unfortunately this does not seem like it is going to be quick and easy to fix. It may take a while longer before I can get around to it.

[tomtau]

@hermanventer do you have any suggestions for a temporary workaround?

[hermanventer]

In general, the way to work around prover limitations is to add assumptions. So if you can track down the expression that fails when sent to the SMT solver, you can assume it, which means that it won't be sent to the solver.

This is a bit harder than it might seem, however, since the expression might be an implicit precondition of some code from a third party library that is not under your control.

[hermanventer]

This appears to be fixed now.