Semantics of triggers and smt.CASE_SPLIT=3

[fpoli]

Is there a Boogie language semantic reason behind the choice of setting Z3's smt.CASE_SPLIT parameter to 3, or is that value just the result of some performance tuning?

The reason I'm looking into this is that I'm trying to understand if in Boogie it's possible for quantifier triggers to "travel back in time". For example, consider the following program. To prove (1) the solver would need to instantiate the axiom matching the trigger on a statement that comes later in the CFG (2). This notion of time is lost when computing the WLP; both foo(x) and bar(x) end up in the same (assert ...) SMT statement. Still, Boogie reports a verification error because smt.CASE_SPLIT=3 inhibits the quantifier instantiation that I described. I'm wondering if this is intentional.

function foo(x: int): int;
function bar(x: int): int;

axiom (forall x: int :: { bar(x) } bar(x) > 0 && foo(x) == 42);

procedure test(x: int)
{
    assert foo(x) == 42;  // (1)
    assert bar(x) > 0;    // (2)
}

The program above, verified with different settings (boogie program.bpl /proverOpt:O:smt.CASE_SPLIT=<value>):

smt.CASE_SPLIT	Verification
0 - case split based on variable activity	succeeds
1 - similar to 0, but delay case splits created during the search	succeeds	Z3's default
2 - similar to 0, but cache the relevancy	succeeds
3 - case split based on relevancy (structural splitting)	fails	Boogie's default
4 - case split on relevancy and activity	fails
5 - case split on relevancy and current goal	fails
6 - activity-based case split with theory-aware branching activity	succeeds

[bkragl]

Boogie does not set smt.case_split anymore since #197. The following code is where Boogie sets the minimum necessary Z3 options. Are you running a very old Boogie?

boogie/Source/Provers/SMTLib/Z3.cs

Lines 61 to 71 in 76b6a37

	public static void SetDefaultOptions(SMTLibSolverOptions options)
	{
	options.AddWeakSmtOption("smt.mbqi", "false"); // default: true
	// {:captureState} does not work with compressed models
	options.AddWeakSmtOption("model.compact", "false"); // default: false
	options.AddWeakSmtOption("model.v2", "true"); // default: false
	// Make sure we get something that is parsable as a bitvector
	options.AddWeakSmtOption("pp.bv_literals", "false"); // default: true
	}

Dafny still sets the cocktail of options that Boogie used to set. I think all of them are performance tuning, no semantic reason.
https://github.com/dafny-lang/dafny/blob/3857e3bce6637013e4ce8a7ac5edafed15916647/Source/DafnyCore/DafnyOptions.cs#L1151-L1173

Coincidentally, I saw that 2 days ago in dafny-lang/dafny#3233 that Dafny changed to only set smt.case_split for Z3 versions 4.8.5 and below. See the discussion there.

[fpoli]

Thanks Bernard, I didn't notice that recent Boogie versions no longer set all those options. I was using a very old Boogie version by mistake.

The discussion in dafny-lang/dafny#3233 is useful. One of the reasons the Carbon verifier of Viper uses a slightly old Boogie version is that recent versions appear to be a bit slower. However, maybe it's because Carbon has its own set of Z3 options, inspired by old Boogie/Dafny versions. Removing those options also from Carbon sounds like a good thing to try.

[gauravpartha]

As a clarification: Carbon itself sets case_split=3 (like Dafny). Carbon indeed uses an old Boogie version (but one that is newer than #197). In the next Carbon release (which should happen by next month), we will be upgrading to Boogie version 2.15.9 (7449a7a). I agree that it makes sense to try out different options for Carbon based on dafny-lang/dafny#3233.