Running Silicon

Jump to bottom

Malte Schwerhoff edited this page May 8, 2022 · 3 revisions

General

Silicon has various and mostly experimental command-line options. Run Silicon with --help for details.
Depending on the used shell (e.g. Windows CMD, bash, ...), passing arguments to --z3Args and --z3ConfigArgs can be tricky because of the mandatory quotation marks (") that must surround the argument.
- Windows CMD: try --z3Args "\"-smt2 -t:500\"", or --z3ConfigArgs "\"smt.macro_finder=true smt.arith.nl.gb=false\""
- Sbt console: try --z3Args "\\\"-smt2 -t:500\\\"", or --z3ConfigArgs "\\\"smt.macro_finder=true smt.arith.nl.gb=false\\\""

Sbt

Run only tests with specific tags, e.g. testOnly -- -n functions
Run only a specific test suite, e.g. testOnly *SiliconTestsMoreCompleteExhale
Pass Silicon-specific options:
- E.g. testOnly -- -n arithmetic.vpr -Dsilicon:logLevel=debug to run certain tests with specific options
- E.g. testOnly -- -Dsilicon:logLevel=debug to run all tests with specific options
Include and exclude tests: E.g. testOnly -- -n termination/ -l termination/methods/ will include all tests anywhere under directory termination, but exclude those anywhere under termination/methods