Practicing symbolic testing
Firstly, let's get back to our simple example that we wrote to test whether the symtest command works. As a reminder, this is what it looked like:
namespace NSMain;
entrypoint function main(arg: Int): Int {
return arg * 2;
}
When you ran the symbolic testing, you saw information about the possible errors that were detected. It is time to check these errors and see whether there is anything we can do about them. In order to make the SymTest tool generate some failing inputs, you need to pass the -m flag:
$ symtest main.bsq -m
After running this command, you should see an output similar to this one:
Symbolic testing of Bosque sources in files: main.bsq ... Transpiling Bosque assembly to bytecode with entrypoint of NSMain::main... Running z3 on SMT encoding... Detected possible errors! Attempting to extract inputs... arg = 4503599627370496
Note the Attempting to extract inputs… part...