Home

Command line options and defaults

Running --help will get you a printout like this:

Real compilation (compilation of real programs)
--functions=f1:f2    Limit verification to f1, f2,...
--pathError          Check also the path error (default is to not check)
--precision=single   Which precision to assume of the underlyingfloating-point arithmetic:
                      single, double, doubledouble, quaddouble or all (sorted from smallest).
--specGen            Generate specs also for functions without postconditions (default is not)
--z3Only             Let Z3 loose on the full constraint - at your own risk.
--z3Timeout=1000     Timeout for Z3 in milliseconds.

Since this and its consequences may not be self-explanatory, here is some more info:

• --functions=f1:f2 will ignore all functions except the listed one. This also means that the ignored function's bodies are not available for function inlining.
• --precision=single selects which precision(s) to consider. Default is double. The order of precisions determines which precisions you prefer, first is best.
• --z3Only Rosa also supports a direct translation from the floating-point constraint, without any approximation. Since the constraint can be very large and complex, Z3 may get stuck.