search

rems-project / sail

Sail architecture definition language
Other
588 stars 102 forks source link

SMT solver returned unexpected status 1 #307

Closed Timmmm closed 1 year ago

Timmmm commented 1 year ago

I am using Sail from commit 27a183e033f858d957758fef8ce34f71319d79c6.

This test.sail

default Order dec

$include <vector_dec.sail>

function foo() -> bits(definitelydoesntexist) = {
  0b0
}

gives this error

❯ sail -c test.sail
Error:
SMT solver returned unexpected status 1

This was quite tricky to track down. It gives no clue to the location and my actual error was a typo of bits(r) instead of bits(4) - not obvious!

bacam commented 1 year ago

Thanks, I've added the missing check. Now, just waiting on the CI before merging.