avanhatt / wasmtime

Standalone JIT-style runtime for WebAssembly, using Cranelift
https://wasmtime.dev/
Apache License 2.0
0 stars 1 forks source link

veri: fix bug in BVShr type inference #95

Closed mmcloughlin closed 8 months ago

mmcloughlin commented 8 months ago

This PR fixes a bug in the Solver in dynamic width mode and onlywidths true, where the y operand of a BVShr expression will not be visited. This can cause type inference to fail. This problem came up when trying to use a Sail-generated specification that contained a concat expression in the right-hand-side operand.