SVA: implement ranged s_eventually operator
#691
Conversation
This adds a BMC encoding for the ranged variant of the s_eventually operator.
kroening
force-pushed
the
sva_ranged_s_eventually
branch
from
2e85f45 to
1bf5a17
Compare
| else if(expr.id() == ID_sva_ranged_s_eventually) | ||
| { |
There was a problem hiding this comment.
Not that this change makes the decisive difference, but: instantiate_rec has become very very long and could do with breaking into smaller functions. Perhaps this opportunity could be taken to at least move this case to a function of its own?
There was a problem hiding this comment.
Will do. What bugs me most is the duplication between instantiate_word_level.cpp and property.cpp.
| mp_integer to; | ||
|
|
||
| if(upper.id() == ID_infinity) | ||
| { | ||
| throw ebmc_errort() | ||
| << "failed to convert SVA s_eventually to index (infinity)"; | ||
| } | ||
| else |
There was a problem hiding this comment.
I believe this check could be done earlier so that to could use RAII and also its handling would be symmetric to that of from.
There was a problem hiding this comment.
RAII won't do it -- it's perfectly fine to initialize with infinity. What's missing here is the comment "the normalizer has rewritten this". I'll implement the case, since I want to rely less on the normalizer doing stuff. It's just one line.
This adds a BMC encoding for the ranged variant of the
s_eventuallyoperator.