prove-rs / z3.rs

Rust bindings for the Z3 solver.
347 stars 110 forks source link

`Int::power(&Int)` returns `Int` but it is `Real` #220

Closed HKalbasi closed 1 year ago

HKalbasi commented 1 year ago

I got a called Result::unwrap() on an Err value: SortDiffers { left: Real, right: Int } when used equality on result of power with another int expression.