search

elliottt / easy-smt

Easy SMT solver interaction
Apache License 2.0
24 stars 4 forks source link

Index out of bounds error when calling `ctx.assert` #10

Closed rachitnigam closed 1 year ago

rachitnigam commented 1 year ago

I'm using the library to generate and discharge some assertions but it seems to throw a bounds-check error in an unsafe code block. Not sure how I should debug it since it seems related to the arena-based interning.

Reproduction

git clone https://github.com/cucapra/filament.git
cd filament
git fetch --all
git checkout f53494b
cargo run -- primitives/state.fil --show-ir

The program errors out with:

thread 'main' panicked at 'index out of bounds: the len is 77 but the index is 87'
elliottt commented 1 year ago

I'll take a look tonight, thanks for the report!

On Wed, May 31, 2023, 17:24 Rachit Nigam @.***> wrote:

I'm using the library to generate and discharge some assertions but it seems to throw a bounds-check error in an unsafe code block. Not sure how I should debug it since it seems related to the arena-based interning. Reproduction

git clone https://github.com/cucapra/filament.git cd filament git fetch --all git checkout discharge cargo run -- primitives/state.fil --show-ir

The program errors out with:

thread 'main' panicked at 'index out of bounds: the len is 77 but the index is 87'

— Reply to this email directly, view it on GitHub https://github.com/elliottt/easy-smt/issues/10, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAAFRNH4D7C65WPQK2S73ATXI7OL5ANCNFSM6AAAAAAYWFPVQA . You are receiving this because you are subscribed to this thread.Message ID: @.***>

rachitnigam commented 1 year ago

Figured out the problem! I was mistakenly using two different Context objects which was causing the problem!

elliottt commented 1 year ago

Ah, that would do it!

On Wed, May 31, 2023, 18:12 Rachit Nigam @.***> wrote:

Closed #10 https://github.com/elliottt/easy-smt/issues/10 as completed.

— Reply to this email directly, view it on GitHub https://github.com/elliottt/easy-smt/issues/10#event-9396962490, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAAFRNG7UIDCLFFAYHZUOQ3XI7T6HANCNFSM6AAAAAAYWFPVQA . You are receiving this because you commented.Message ID: @.***>