MrChico
MrChico
I believe you need to use the full qualified path of the contract, see https://solidity.readthedocs.io/en/v0.6.11/contracts.html?highlight=library#libraries
I think this is a shell string quoting issue. Try this: ``` SOLC_FLAGS='--libraries "Controller:0x388be118C18Df3180F4FE0f0A19A4a4180ff45bC SelectiveLiquidity:0x970CC9F79B28662c198167f589af7f854b3BD3F8 ProportionalLiquidity:0x01F6252E54a272145CB2d035bF6a13DBD269426f Shells:0x725C05594edc80E48E8bE2220C9ef02c4d28F617 Swaps:0x9665552d314AC6d8004d3b8f53f6612Af4eF5760"' dapp build --extract ```
> with that, there isn't an error, but nor is any linking performed I guess you need to `export` SOLC_FLAGS
I think this procedure is a bit broader than just counterexample generation. The procedure you are describing is essentially a backtracing to the initial state from the goal, and so...
Here's how we wrote a loop invariant in the act flavor for rpow: ```act behaviour rpow-loop of Jug lemma // 0a3a => 0a7e pc 2618 => 2686 for all Half...
It should be noted that by treating anything in the changeset as a new, arbitrary value, we are essentially forgetting information, which is a little dangerous – this is an...
another alternative would be to not allow environment variables in invariant blocks at all. Restricting invariants to be formulas over state variables would make the matter moot. I think having...
This opens some questions about modules and imports that I think requires a bit of thought
for act
hmm, that option seems even more cumbersome than keeping around the position information in the refined context