option `--symbolic-execution` not listed

[grosu]

in krun --help:

Usage: krun [options] <file>
  Options:
    --bound
       The number of desired solutions for search.
    --color
       Use colors in output. Default is on.
    --config-parser, -p
       Command used to parse configuration variables. Default is "kast --parser
       ground -e". See description of --parser. For example, -cpPGM="kast"
       specifies that the configuration variable $PGM should be parsed with the
       command "kast".
       Syntax: --config-parserkey=value
       Default: {}
    --config-var, -c
       Specify values for variables in the configuration.
       Syntax: --config-varkey=value
       Default: {}
    --debug
       Print debugging output messages
       Default: false
    --depth
       The maximum number of computational steps to execute or search the
       definition for.
    --directory, -d
       Path to the directory in which the kompiled K definition resides. The
       default is the unique, only directory with the suffix '-kompiled' in the
       current directory. A definition may also be specified with the
       'KRUN_COMPILED_DEF' environment variable, in which case it is used if the
       option is not specified on the command line.
    --exit-code
       Specify a term containing a named integer variable which will be used as
       the exit status of krun.
    --graph
       Displays the search graph generated by the last search.
       Default: false
    --help, -h
       Print this help message
       Default: false
    --help-experimental, -X
       Print help on non-standard options.
       Default: false
    --io
       Use real IO when running the definition. Defaults to true.
    --output, -o
       How to display krun results. <mode> is either
       [pretty|sound|kast|binary|none|no-wrap].
       Default: PRETTY
    --parser
       Command used to parse programs. Default is "kast"
    --pattern
       Specify a term and/or side condition that the result of execution or
       search must match in order to succeed. Return the resulting matches as a
       list of substitutions. In conjunction with it you can specify other 2
       options that are optional: bound (the number of desired solutions) and
       depth (the maximum depth of the search).
    --search
       In conjunction with it you can specify 3 options that are optional:
       pattern (the pattern used for search), bound (the number of desired
       solutions) and depth (the maximum depth of the search).
       Default: false
    --search-all
       Same as --search but return all matching states, even if --depth is not
       provided.
       Default: false
    --search-final
       Same as --search but only return final states, even if --depth is
       provided.
       Default: false
    --search-one-or-more-steps
       Same as --search-all but exclude initial state, even if it matches.
       Default: false
    --search-one-step
       Same as --search but search only one transition step.
       Default: false
    --term
       Input argument will be parsed with the specified parser and used as the
       sole input to krun.
       Default: false
    --terminal-color
       Background color of the terminal. Cells won't be colored in this color.
       Default: black
    --verbose, -v
       Print verbose output messages
       Default: false
    --version
       Print version information
       Default: false
    --warnings, -w
       Warning level. Values: [all|normal|none]
       Default: NORMAL
    --warnings-to-errors, -w2e
       Convert warnings to errors.
       Default: false

[dwightguth]

I believe it is listed as an experimental option... Shouldn't be too hard to break the JavaExecutionOptions class into separate experimental and nonexperimental versions.

On Thu, Apr 9, 2015 at 2:51 PM, Grigore Rosu notifications@github.com wrote:

in krun --help:

Usage: krun [options] Options: --bound The number of desired solutions for search. --color Use colors in output. Default is on. --config-parser, -p Command used to parse configuration variables. Default is "kast --parser ground -e". See description of --parser. For example, -cpPGM="kast" specifies that the configuration variable $PGM should be parsed with the command "kast". Syntax: --config-parserkey=value Default: {} --config-var, -c Specify values for variables in the configuration. Syntax: --config-varkey=value Default: {} --debug Print debugging output messages Default: false --depth The maximum number of computational steps to execute or search the definition for. --directory, -d Path to the directory in which the kompiled K definition resides. The default is the unique, only directory with the suffix '-kompiled' in the current directory. A definition may also be specified with the 'KRUN_COMPILED_DEF' environment variable, in which case it is used if the option is not specified on the command line. --exit-code Specify a term containing a named integer variable which will be used as the exit status of krun. --graph Displays the search graph generated by the last search. Default: false --help, -h Print this help message Default: false --help-experimental, -X Print help on non-standard options. Default: false --io Use real IO when running the definition. Defaults to true. --output, -o How to display krun results. is either [pretty|sound|kast|binary|none|no-wrap]. Default: PRETTY --parser Command used to parse programs. Default is "kast" --pattern Specify a term and/or side condition that the result of execution or search must match in order to succeed. Return the resulting matches as a list of substitutions. In conjunction with it you can specify other 2 options that are optional: bound (the number of desired solutions) and depth (the maximum depth of the search). --search In conjunction with it you can specify 3 options that are optional: pattern (the pattern used for search), bound (the number of desired solutions) and depth (the maximum depth of the search). Default: false --search-all Same as --search but return all matching states, even if --depth is not provided. Default: false --search-final Same as --search but only return final states, even if --depth is provided. Default: false --search-one-or-more-steps Same as --search-all but exclude initial state, even if it matches. Default: false --search-one-step Same as --search but search only one transition step. Default: false --term Input argument will be parsed with the specified parser and used as the sole input to krun. Default: false --terminal-color Background color of the terminal. Cells won't be colored in this color. Default: black --verbose, -v Print verbose output messages Default: false --version Print version information Default: false --warnings, -w Warning level. Values: [all|normal|none] Default: NORMAL --warnings-to-errors, -w2e Convert warnings to errors. Default: false

— Reply to this email directly or view it on GitHub https://github.com/kframework/k/issues/1439.