m-carrasco / TinyBCT

MIT License
3 stars 2 forks source link

Possibly omit additional subtyping axioms when not necessary #41

Open rcastano opened 6 years ago

rcastano commented 6 years ago

The recent fix for issue #29 causes TinyBCT to generate larger Boogie files (longer axioms). We should try to find a way to resort to shorter axioms when possible.

This might deserve a more involved discussion and evaluation of the actual impact on performance.