Dimitar Bounov
Dimitar Bounov
Good question @Melvillian - I think I didn't give enough detail in the description. Currently `--user-asert-mode` supports two possible options - `log` and `mstore`. These control exactly how user assertion...
Is this in the case where there is a `sum` operator over the map, but no `forall`?
@naps62 unfortunately that can't be expressed with scribble at the moment. To say that, you need a map function, that maps each struct Account in the `accounts` map, into its...
@nettrino you're correct - it is not currently possible. However could you post a sample of what you would like supported? If there is enough interest in this feature, and...
I am not sure if I understand everything here. If you just want to check that `msg.value > Rv` JUST BEFORE the `registerEntity` function, you can do something like this:...
Does this answer your question? Or is it something different?
Haven't heard anything on this for a while, so closing. If this is still an issue please reopen
@axic thanks for pointing this out! Do you have a sample/link to a codebase so we can reproduce it too? And yeah, this looks like its related to the fix...
Ok. Will try to look at the code and find anything suspicious
I was able to reproduce the issue by trying to look-up an identifier that doesn't exist. Here are the samples: A.sol: ``` import "./B.sol"; /// #invariant dummy > 0; contract...