Does random_seed affect the initial state of parameters in an implementation?

[tbean79]

I'm interested in leveraging the random_seed attribute in order to have variety in the values returned by z3's counterexample. For instance, this implementation has 3 parameters of different types.

implementation {:random_seed N} Impl$$_module.__default.isOddLength(i#0: int, j#0: Seq Box, k#0: bool) returns (res#0: bool, $_reverifyPost: bool)
{
  var $_Frame: <beta>[ref,Field beta]bool;

  anon0:
    assume {:print "Impl", " | ", "Impl$$_module.__default.isOddLength", " | ", i#0, " | ", j#0, " | ", k#0} true;
    assume {:print "Types", " | ", "int", " | ", "Seq Box", " | ", "bool"} true;
    
    $_Frame := (lambda<alpha> $o: ref, $f: Field alpha :: $o != null && read($Heap, $o, alloc) ==> false);
    $_reverifyPost := false;

    assert false;  // I injected this so I'll get a counterexample
...

No matter what I change the random_seed number N to, the initial state of the counterexample model always has the same values for i#0, j#0, and k#0.

*** STATE <initial>
  $_Frame -> 
  $_reverifyPost -> 
  $Heap -> T@U!val!4
  $Tick -> 
  i#0 -> 
  j#0 -> T@U!val!5
  k#0 -> 
  res#0 -> 
*** END_STATE

Is this due to implementation parameters being immutable? I understand I'm not allowed to havoc these parameters for the same reason. I'm wondering if this is also why z3 doesn't return values within the parameters' domains, no matter what random_seed is specified.

I'm willing to post the whole .bpl file as needed.

[keyboardDrummer]

Have you tried an example where the values of the variables i j and k determine whether the assertion fails or not? I'm not sure whether that would help but to me it seems like a worthwhile experiment.

[tbean79]

This is indeed correct. My error was thinking that the random seed influences what values z3 starts out with as it marches through the implementation. I was planning on z3 spilling those values once it reaches assert false. I realize now this is not how z3 behaves, as it seems to only come up with values as needed to prove an assertion wrong. So a simple assertion like assert false doesn't require much thinking of z3 (and therefore z3 always comes up with default values), whereas an assertion like i#0 % 2 == 0 does (and therefore z3's values are influenced by random_seed).