Running Silicon

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