search

uclid-org / uclid

UCLID5: formal modeling, verification, and synthesis of computational systems
Other
136 stars 32 forks source link

enum pass bugs #87

Open polgreen opened 3 years ago

polgreen commented 3 years ago

The enum->numeric pass needs fixing.

Soundness bug: uclid -e test/test-enum-1.ucl produces different results to uclid test/test-enum-1.ucl

Assertion failure: uclid examples/cpu_induction.ucl -e throws an assertion error.

My guess is that the latter is to do with enums from different modules not being imported correctly. The former, I don't know.

polgreen commented 3 years ago

@kkmc you wrote the enum pass rewriter? Could you look into this please?