Additional Configuration

Config key prefix: <prefix>, e.g., jdart.configs.sample

• max_depth (integer): the maximum depth of the constraints tree. The resulting constraints tree will in no case be deeper than this; explorations which go beyond this depth will simply not be reflected in the tree. A negative value means infinite (default).
• max_alt_depth (integer): the maximum depth of alternation (i.e., constraint negation) in the constraint tree. At the root of every sub-tree which was accessed through a valuation obtained from a constraint solver, the alternation depth increases by one. For unexplored nodes with an alternation depth larger than this value, no constraint solving will be attempted. A negative value means infinite (default).
• max_nesting_depth (integer): Native methods cannot be executed concolically. Their return values (if dependent on symbolic argument values) will be reflected as an (uninterpreted) function in the constraints tree. This option bounds the nesting depth of these function expressions. If this value is exceeded (i.e., a native call is made to a method with a symbolic argument of the specified nesting depth), the symbolic information for the return value is discarded altogether.
• constraints (;-separated list of strings): further constraints to be imposed on the exploration. This is an expression over the overall set of symbolic variables, which will be enforced for every constraint solving step during concolic execution.