search

kframework / k-legacy

The K tools (deprecated, see README)
http://kframework.org
Other
146 stars 61 forks source link

Verification Related Fixes #2324

Closed msaxena2 closed 6 years ago

msaxena2 commented 6 years ago

Helpful Debugging Info for z3 + Missing Case Fix for Fast Rule Matcher.

msaxena2 commented 6 years ago

@nishantjr - Your commits are here too. Please take a look.

msaxena2 commented 6 years ago

@cos @andreistefanescu Please review. The second last commit (abe14ab ) fixes issues with unexpected Z3 queries in the prover.

andreistefanescu commented 6 years ago

@msaxena2 your fix was a good attempt, but this should set the proper constraint just before use. Please review.

msaxena2 commented 6 years ago

@cos @andreistefanescu I was able to get around the issue by slightly changing the semantics of EVM (one of the rules that had an owise attribute was causing the issue). I think we should merge these changes, and deal with issues with owise in a separate PR - using a much simpler definition than EVM.