Dmitry Petukhov
Dmitry Petukhov
> Maybe I did not understand, but if you analyze with `--z3-enabled=true`, the report will show that the enforcement condition is 'always true' z3 isn't working for me; I'm getting:...
From https://github.com/dgpv/bsst/pull/33#issuecomment-2123371113: > I'm doing the first case, so hiding the impossible things would be good for me right now, but the second case is definitely a real thing too....
I am thinking about using branch conditions to show data references. For example, now it is like this: ``` ./bsst-cli 0 lessthan if 5 else 10 endif // =>x add...
Interesting that the report in the previous message shows ``` ============================== Enforced constraints per path: ============================== All valid paths: ---------------- {*} GREATERTHANOREQUAL(wit0, 0) @ 3:L1 {*} LESSTHAN(wit0, 64) @ 7:L2...
https://github.com/ElementsProject/elements/blob/e5ab941489c564cd78845658b8e8688dc56817f5/src/rpc/rawtransaction.cpp#L2896-L2912 the assignment ``` mtx.vin[issuance_input_index].assetIssuance.nAmount = asset_amount; ``` at line 2912 is the same as the assignment at line 2898 neither `asset_amount` nor `assetIssuance.nAmount` seem to be modified between the...