Assertion mode option is broken

[vakaras]

Silicon --help describes the assertion mode option as follows:

--assertionMode  <arg>...                    Determines how assertion
                                                   checks are encoded in SMTLIB.
                                                   Options are 'pp' (push-pop)
                                                   and 'cs' (soft constraints)
                                                   (default: cs).

This help message has at least two mistakes:

• Soft constraints should be specified with sc, not cs.
• The specified default is wrong; Silicon uses push-pop by default.

When sc is passed to Silicon, it crashes with the following error:

  Cause: java.util.concurrent.ExecutionException: viper.silicon.reporting.ProverInteractionFailed: Unexpected output of prover. Expected 'success' but found: (error "line 1383 column 22: invalid expression, unexpected keyword")
Silicon found 1 error in 6,73s:
  [0] Interaction with prover (instance 08) failed: Unexpected output of prover. Expected 'success' but found: (error "line 1383 column 22: invalid expression, unexpected keyword")

[fpoli]

Marco already fixed the second point:

silicon/src/main/scala/Config.scala

Lines 566 to 571 in 2c417ef

	val assertionMode: ScallopOption[AssertionMode] = opt[AssertionMode]("assertionMode",
	descr = ( "Determines how assertion checks are encoded in SMTLIB. Options are "
	+ "'pp' (push-pop) and 'cs' (soft constraints) (default: pp)."),
	default = Some(AssertionMode.PushPop),
	noshort = true
	)(assertionModeConverter)

[marcoeilers]

Fixed in PR #680.