How to run SMTchecker without the pragma

Question

According to documentation pragma experimental SMTchecker won't work for latest versions. It says to use --model-checker-targets "underflow,overflow". But I don't know how. I am new in this field and I have no idea where am I supposed to use the above line. I have installed solc in ubuntu. I could not find any good tutorial on how to use SMTchecker. Documentation says to use --model-checker-tragets, but I don't know where to use it and how to use it.

Answer 1

These parameters need to be passed on the compiler command line. Please make sure you're invoking the compiler binary directly (solc) (or via solc-js - the Standard JSON input also has corresponding settings - but you'd only really do that only if you're writing a JS tool).

For example to run the Overflow example from the tutorial in the docs you'd put the code in a file (let's call it overflow.sol) and run this command in a terminal:

solc overflow.sol \
    --model-checker-targets "underflow,overflow" \
    --model-checker-engine all

(NOTE: the \ symbols are line continuations, you can also remove them and put it all on a single line).

Most tools like frameworks, IDEs, plugins, etc. do not support the new parameters yet so when using them only the old method works. This should change in the near future though - e.g. there's an issue in Remix IDE to add UI for them (#1751).

By the way, the pragma will eventually be removed but likely not before tools actually have at least some support for the new way to run the SMTChecker. As of 0.8.10 the pragma still works fine.